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 set 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
A5: Y in (Tarski-Class X) \ (Rank A) and
A6: for x being set holds
( not x in (Tarski-Class X) \ (Rank A) or not x in Y ) by TARSKI:7;
Tarski-Class X is epsilon-transitive by A1, Th27;
then A8: Y c= Tarski-Class X by A5, ORDINAL1:def 2;
Y c= Rank A

proof

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

end;

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