lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫;
fold normalize X; intros; cases H1;
lemma nat_dedekind_sigma_complete:
∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing →
∀x.x is_supremum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).
intros 5; cases x (s Hs); clear x; letin X ≝ ≪s,Hs≫;
fold normalize X; intros; cases H1;