let X be set ; :: thesis: sup X c= succ (union (On X))
reconsider A = union (On X) as Ordinal by Th7;
On X c= succ A

proof

let x be set ; :: 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 10;
a c= A by A1, ZFMISC_1:92;
hence x in succ A by ORDINAL1:34; :: thesis: verum

end;

hence sup X c= succ (union (On X)) by ORDINAL2:def 7; :: thesis: verum