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 ( A = succ C or succ C in A ) by Th10;
then A2: succ C c= C by A1, Def2;
C in succ C by Th2;
then C c= succ C by Def2;
then succ C = C by A2;
hence contradiction by Th5; :: thesis: verum