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
A4: x in (Tarski-Class X) \ (Rank A) by A3, XBOOLE_0:def 5;
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 A4, TARSKI:7;
A7: Tarski-Class X is epsilon-transitive by A1, Th27;
A8: Y c= Tarski-Class X by A5, A7, ORDINAL1:def 2;
A9: 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
A11: not x in (Tarski-Class X) \ (Rank A) by A6, A10;
thus x in Rank A by A8, A10, A11, XBOOLE_0:def 5; :: thesis: verum

end;

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