let W be set ; :: thesis: ( W is epsilon-transitive implies Rank (card (Tarski-Class W)) = Tarski-Class W )
assume W is epsilon-transitive ; :: thesis: Rank (card (Tarski-Class W)) = Tarski-Class W
then Rank (card (Tarski-Class W)) is_Tarski-Class_of W by Th44;
hence ( Rank (card (Tarski-Class W)) c= Tarski-Class W & Tarski-Class W c= Rank (card (Tarski-Class W)) ) by Th28, CLASSES1:def 4; :: according to XBOOLE_0:def 10 :: thesis: verum