let X be set ; :: thesis: sup X c= succ (union (On X))
reconsider A = union (On X) as Ordinal by Th5;
On X c= succ A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On X or x in succ A )
assume A1: x in On X ; :: thesis: x in succ A
then reconsider a = x as Ordinal by ORDINAL1:def 9;
a c= A by A1, ZFMISC_1:74;
hence x in succ A by ORDINAL1:22; :: thesis: verum
end;
hence sup X c= succ (union (On X)) by ORDINAL2:def 3; :: thesis: verum