alias symbol "leq" = "natural 'less or equal to'".
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).
alias symbol "leq" = "natural 'less or equal to'".
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).