let W be set ; :: thesis: ( W is Tarski & W is epsilon-transitive implies Rank (card W) = W )
assume ( W is Tarski & W is epsilon-transitive ) ; :: thesis: Rank (card W) = W
hence ( Rank (card W) c= W & W c= Rank (card W) ) by Th28, Th31; :: according to XBOOLE_0:def 10 :: thesis: verum