let W, X be set ; :: thesis: ( W is Tarski & X is epsilon-transitive & X in W implies X in Rank (card W) )
assume A1: W is Tarski ; :: thesis: ( not X is epsilon-transitive or not X in W or X in Rank (card W) )
assume A2: X is epsilon-transitive ; :: thesis: ( not X in W or X in Rank (card W) )
assume X in W ; :: thesis: X in Rank (card W)
then card X in card W by A1, Th1;
then A3: card (the_rank_of X) in card W by A2, Th42, ORDINAL1:22;
card (card W) = card W ;
then the_rank_of X in card W by A3, CARD_3:59;
then A4: Rank (the_rank_of X) in Rank (card W) by 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