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 )
assume A1: X is unbounded ; :: thesis: not X is empty
consider B1 being Element of A;
consider C being Ordinal such that
A2: C in X and
B1 c= C by A1, Th7;
thus not X is empty by A2; :: thesis: verum