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

proof

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;

X c= sup X by Th2;
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