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
A4: Y in (Tarski-Class X) \ (Rank A) and
A5: 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 & Y in Tarski-Class X ) by A1, A4, Th27;
then A6: Y c= Tarski-Class X by 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 x in Y ; :: thesis: x in Rank A
then ( not x in (Tarski-Class X) \ (Rank A) & x in Tarski-Class X ) by A5, A6;
hence x in Rank A by XBOOLE_0:def 5; :: thesis: verum

end;

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