let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A st not X is empty & ( for B1 being Ordinal st B1 in X holds

ex B2 being Ordinal st

( B2 in X & B1 in B2 ) ) holds

sup X is limit_ordinal infinite Ordinal

let X be Subset of A; :: thesis: ( not X is empty & ( for B1 being Ordinal st B1 in X holds

ex B2 being Ordinal st

( B2 in X & B1 in B2 ) ) implies sup X is limit_ordinal infinite Ordinal )

assume not X is empty ; :: thesis: ( ex B1 being Ordinal st

( B1 in X & ( for B2 being Ordinal holds

( not B2 in X or not B1 in B2 ) ) ) or sup X is limit_ordinal infinite Ordinal )

then A1: ex x being object st x in X by XBOOLE_0:def 1;

assume A2: for B1 being Ordinal st B1 in X holds

ex B2 being Ordinal st

( B2 in X & B1 in B2 ) ; :: thesis: sup X is limit_ordinal infinite Ordinal

A3: for C being Ordinal st C in sup X holds

succ C in sup X

then reconsider SUP = sup X as limit_ordinal non empty Ordinal by A3, A1, ORDINAL1:28;

SUP is limit_ordinal infinite Ordinal ;

hence sup X is limit_ordinal infinite Ordinal ; :: thesis: verum

ex B2 being Ordinal st

( B2 in X & B1 in B2 ) ) holds

sup X is limit_ordinal infinite Ordinal

let X be Subset of A; :: thesis: ( not X is empty & ( for B1 being Ordinal st B1 in X holds

ex B2 being Ordinal st

( B2 in X & B1 in B2 ) ) implies sup X is limit_ordinal infinite Ordinal )

assume not X is empty ; :: thesis: ( ex B1 being Ordinal st

( B1 in X & ( for B2 being Ordinal holds

( not B2 in X or not B1 in B2 ) ) ) or sup X is limit_ordinal infinite Ordinal )

then A1: ex x being object st x in X by XBOOLE_0:def 1;

assume A2: for B1 being Ordinal st B1 in X holds

ex B2 being Ordinal st

( B2 in X & B1 in B2 ) ; :: thesis: sup X is limit_ordinal infinite Ordinal

A3: for C being Ordinal st C in sup X holds

succ C in sup X

proof

X c= sup X
by Th2;
let C be Ordinal; :: thesis: ( C in sup X implies succ C in sup X )

assume C in sup X ; :: thesis: succ C in sup X

then consider B3 being Ordinal such that

A4: B3 in X and

A5: C c= B3 by ORDINAL2:21;

consider B2 being Ordinal such that

A6: B2 in X and

A7: B3 in B2 by A2, A4;

C in B2 by A5, A7, ORDINAL1:12;

then A8: succ C c= B2 by ORDINAL1:21;

B2 in sup X by A6, ORDINAL2:19;

hence succ C in sup X by A8, ORDINAL1:12; :: thesis: verum

end;assume C in sup X ; :: thesis: succ C in sup X

then consider B3 being Ordinal such that

A4: B3 in X and

A5: C c= B3 by ORDINAL2:21;

consider B2 being Ordinal such that

A6: B2 in X and

A7: B3 in B2 by A2, A4;

C in B2 by A5, A7, ORDINAL1:12;

then A8: succ C c= B2 by ORDINAL1:21;

B2 in sup X by A6, ORDINAL2:19;

hence succ C in sup X by A8, ORDINAL1:12; :: thesis: verum

then reconsider SUP = sup X as limit_ordinal non empty Ordinal by A3, A1, ORDINAL1:28;

SUP is limit_ordinal infinite Ordinal ;

hence sup X is limit_ordinal infinite Ordinal ; :: thesis: verum