let W be set ; :: thesis: ( W is Tarski & W is epsilon-transitive implies W c= Rank (card W) )
assume A1: ( W is Tarski & W is epsilon-transitive ) ; :: thesis: W c= Rank (card W)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in Rank (card W) )
assume x in W ; :: thesis: x in Rank (card W)
then the_rank_of x in W by A1, Th30;
then ( the_rank_of x in On W & On W = card W ) by A1, Th10, ORDINAL1:def 10;
then ( x c= Rank (the_rank_of x) & Rank (the_rank_of x) in Rank (card W) ) by CLASSES1:42, CLASSES1:def 8;
hence x in Rank (card W) by CLASSES1:47; :: thesis: verum