+(* 3.28 *)
+definition liminf ≝
+ λR.λml:mlattice R.λxn:sequence ml.λx:ml.
+ ∃alpha:sequence ml.
+ (∀k.strong_inf ml (ank ?? xn k) (alpha k)) ∧ strong_sup ml alpha x.
+
+definition limsup ≝
+ λR.λml:mlattice R.λxn:sequence ml.λx:ml.
+ ∃alpha:sequence ml.
+ (∀k.strong_sup ml (bnk ?? xn k) (alpha k)) ∧ strong_inf ml alpha x.
+
+(* 3.29 *)
+alias symbol "and" = "constructive and".
+definition lim ≝
+ λR.λml:mlattice R.λxn:sequence ml.λx:ml.
+ (*∃y,z.*)limsup ?? xn x ∧ liminf ?? xn x(* ∧ y ≈ x ∧ z ≈ x*).
+
+(* 3.30 *)
+lemma lim_uniq: ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
+ lim ?? xn x → xn ⇝ x.
+intros (R ml xn x Hl);
+unfold in Hl; unfold limsup in Hl; unfold liminf in Hl;
+(* decompose; *)
+elim Hl (low Hl_); clear Hl;
+elim Hl_ (up Hl); clear Hl_;
+elim Hl (Hl_ E1); clear Hl;
+elim Hl_ (Hl E2); clear Hl_;
+elim Hl (H1 H2); clear Hl;
+elim H1 (alpha Halpha); clear H1;
+elim H2 (beta Hbeta); clear H2;
+apply (sandwich ?? alpha beta);
+[1: intro m; elim Halpha (Ha5 Ha6); clear Halpha;
+ lapply (sup_increasing ????? Ha6) as Ha7;