let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds
( X is bounded iff ex B1 being Ordinal st
( B1 in A & X c= B1 ) )
let X be Subset of A; :: thesis: ( X is bounded 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 Th2;
A = sup A by ORDINAL2:18;
then ( sup X <> A iff sup X in A ) by A1, ORDINAL1:11, ORDINAL2:22;
hence ( X is bounded implies ex B1 being Ordinal st
( B1 in A & X c= B1 ) ) by A2; :: thesis: ( ex B1 being Ordinal st
( B1 in A & X c= B1 ) implies X is bounded )
given B1 being Ordinal such that A3: B1 in A and
A4: X c= B1 ; :: thesis: X is bounded
sup X c= sup B1 by A4, ORDINAL2:22;
then sup X c= B1 by ORDINAL2:18;
hence X is bounded by A3, ORDINAL1:12; :: thesis: verum