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: ( sup X c< A iff ( sup X c= A & sup X <> A ) ) by XBOOLE_0:def 8;
A2: X c= sup X by Th3;
A = sup A by ORDINAL2:18;
then ( sup X <> A iff sup X in A ) by A1, ORDINAL1:11, ORDINAL2:22;
hence ( not X is unbounded implies ex B1 being Ordinal st
( B1 in A & X c= B1 ) ) by A2, Def4; :: thesis: ( ex B1 being Ordinal st
( B1 in A & X c= B1 ) implies not X is unbounded )
given B1 being Ordinal such that A3: B1 in A and
A4: X c= B1 ; :: thesis: not X is unbounded
A5: ( not X is unbounded iff sup X <> A ) by Def4;
sup X c= sup B1 by A4, ORDINAL2:22;
then sup X c= B1 by ORDINAL2:18;
hence not X is unbounded by A5, A3, ORDINAL1:12; :: thesis: verum