let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A st X is unbounded holds

not X is empty

let X be Subset of A; :: thesis: ( X is unbounded implies not X is empty )

set B1 = the Element of A;

assume X is unbounded ; :: thesis: not X is empty

then ex C being Ordinal st

( C in X & the Element of A c= C ) by Th6;

hence not X is empty ; :: thesis: verum

not X is empty

let X be Subset of A; :: thesis: ( X is unbounded implies not X is empty )

set B1 = the Element of A;

assume X is unbounded ; :: thesis: not X is empty

then ex C being Ordinal st

( C in X & the Element of A c= C ) by Th6;

hence not X is empty ; :: thesis: verum