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