let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds
( not X is unbounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
let X be Subset of A; :: thesis: ( not X is unbounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
A1: X c= sup X by Th3;
A2: A = sup A by ORDINAL2:26;
A3: ( not X is unbounded iff sup X <> A ) by Def4;
( sup X c< A iff ( sup X c= A & sup X <> A ) ) by XBOOLE_0:def 8;
then ( sup X <> A iff sup X in A ) by A2, ORDINAL1:21, ORDINAL2:30;
hence ( not X is unbounded implies ex B1 being Ordinal st
( B1 in A & X c= B1 ) ) by A1, Def4; :: thesis: ( ex B1 being Ordinal st
( B1 in A & X c= B1 ) implies not X is unbounded )
given B1 being Ordinal such that A4: B1 in A and
A5: X c= B1 ; :: thesis: not X is unbounded
sup X c= sup B1 by A5, ORDINAL2:30;
then sup X c= B1 by ORDINAL2:26;
hence not X is unbounded by A3, A4, ORDINAL1:22; :: thesis: verum