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

proof

assume A in succ C ; :: thesis: A c= C
then ( A in C or A in {C} ) by XBOOLE_0:def 3;
hence A c= C by Def2, TARSKI:def 1; :: thesis: verum

end;

assume A1: A c= C ; :: thesis: A in succ C
assume not A in succ C ; :: thesis: contradiction
then A2: ( A = succ C or succ C in A ) by Th24;
C in succ C by Th10;
then A3: C c= succ C by Def2;
succ C c= C by A1, A2, Def2;
then succ C = C by A3, XBOOLE_0:def 10;
hence contradiction by Th14; :: thesis: verum