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