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 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, A2, Th30;
then A3: the_rank_of x in On W by ORDINAL1:def 10;
On W = card W by A1, Th10;
then A4: Rank (the_rank_of x) in Rank (card W) by A3, CLASSES1:42;
x c= Rank (the_rank_of x) by CLASSES1:def 8;
hence x in Rank (card W) by A4, CLASSES1:47; :: thesis: verum