let X be set ; :: thesis: for A being Ordinal st X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) holds
Tarski-Class X c= Rank A
let A be Ordinal; :: thesis: ( X is epsilon-transitive & (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) implies Tarski-Class X c= Rank A )
assume that
A1: X is epsilon-transitive and
A2: (Rank A) /\ (Tarski-Class X) = (Rank (succ A)) /\ (Tarski-Class X) ; :: thesis: Tarski-Class X c= Rank A
given x being object such that A3: ( x in Tarski-Class X & not x in Rank A ) ; :: according to TARSKI:def 3 :: thesis: contradiction
x in (Tarski-Class X) \ (Rank A) by A3, XBOOLE_0:def 5;
then consider Y being set such that
A4: Y in (Tarski-Class X) \ (Rank A) and
A5: for x being object holds
( not x in (Tarski-Class X) \ (Rank A) or not x in Y ) by TARSKI:3;
A6: Y c= Tarski-Class X by A4, ORDINAL1:def 2, A1, Th23;
Y c= Rank A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in Rank A )
assume A7: x in Y ; :: thesis: x in Rank A
then not x in (Tarski-Class X) \ (Rank A) by A5;
hence x in Rank A by A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

then Y in Rank (succ A) by Th32;
then A8: Y in (Rank (succ A)) /\ (Tarski-Class X) by A4, XBOOLE_0:def 4;
not Y in Rank A by A4, XBOOLE_0:def 5;
hence contradiction by A2, A8, XBOOLE_0:def 4; :: thesis: verum