let W be set ; :: thesis: ( W is epsilon-transitive implies Rank (card (Tarski-Class W)) is_Tarski-Class_of W )
A1: W in Tarski-Class W by CLASSES1:2;
assume W is epsilon-transitive ; :: thesis: Rank (card (Tarski-Class W)) is_Tarski-Class_of W
hence ( W in Rank (card (Tarski-Class W)) & Rank (card (Tarski-Class W)) is Tarski ) by A1, Th39, Th43; :: according to CLASSES1:def 3 :: thesis: verum