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 for a being object st a in {A} holds
a in B by TARSKI:def 1;
then A2: {A} c= B ;
A c= B by A1, Def2;
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 Th2;
hence A in B by A3; :: thesis: verum