let W be set ; :: thesis: ( W is Tarski & W is epsilon-transitive implies W c= Rank (card W) )
assume that
A1: W is Tarski and
A2: W is epsilon-transitive ; :: thesis: W c= Rank (card W)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in Rank (card W) )
reconsider xx = x as set by TARSKI:1;
assume x in W ; :: thesis: x in Rank (card W)
then the_rank_of xx in W by A1, A2, Th29;
then A3: the_rank_of xx in On W by ORDINAL1:def 9;
On W = card W by A1, Th9;
then A4: Rank (the_rank_of xx) in Rank (card W) by A3, CLASSES1:36;
xx c= Rank (the_rank_of xx) by CLASSES1:def 9;
hence x in Rank (card W) by A4, CLASSES1:41; :: thesis: verum