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

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;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