let A be limit_ordinal Ordinal; :: thesis: for X being set st X c= A & sup X = A holds
union X = A
let X be set ; :: thesis: ( X c= A & sup X = A implies union X = A )
assume X c= A ; :: thesis: ( not sup X = A or union X = A )
then A1: union X c= union A by ZFMISC_1:77;
assume A2: sup X = A ; :: thesis: union X = A
thus union X c= A by A1, ORDINAL1:def 6; :: according to XBOOLE_0:def 10 :: thesis: A c= union X
thus A c= union X :: thesis: verum
proof
let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in A or X1 in union X )
assume A3: X1 in A ; :: thesis: X1 in union X
reconsider X2 = X1 as Ordinal by A3;
succ X2 in A by A3, ORDINAL1:28;
then A4: ex B being Ordinal st
( B in X & succ X2 c= B ) by A2, ORDINAL2:21;
X2 in succ X2 by ORDINAL1:6;
hence X1 in union X by A4, TARSKI:def 4; :: thesis: verum
end;