let A be Ordinal; :: thesis: union (succ A) = A
thus union (succ A) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= union (succ A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (succ A) or x in A )
assume x in union (succ A) ; :: thesis: x in A
then consider X being set such that
A1: x in X and
A2: X in succ A by TARSKI:def 4;
reconsider X = X as Ordinal by A2;
X c= A by A2, ORDINAL1:22;
hence x in A by A1; :: thesis: verum

end;

thus A c= union (succ A) by ORDINAL1:6, ZFMISC_1:74; :: thesis: verum