let A, B be Ordinal; :: thesis: ( A in B iff succ A c= B )
thus ( A in B implies succ A c= B ) :: thesis: ( succ A c= B implies A in B )

proof

assume A1: A in B ; :: thesis: succ A c= B
then A2: A c= B by Def2;
for a being set st a in {A} holds
a in B by A1, TARSKI:def 1;
then {A} c= B by TARSKI:def 3;
hence succ A c= B by A2, XBOOLE_1:8; :: thesis: verum

end;

assume A3: succ A c= B ; :: thesis: A in B
A in succ A by Th10;
hence A in B by A3; :: thesis: verum