let W, X be set ; :: thesis: ( W is Tarski & X is epsilon-transitive & X in W implies X in Rank (card W) )
assume W is Tarski ; :: thesis: ( not X is epsilon-transitive or not X in W or X in Rank (card W) )
then A1: W is subset-closed ;
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 ( card (the_rank_of X) in card W & card (card W) = card W & card W = card W ) by A2, Th42, ORDINAL1:22;
then the_rank_of X in card W by CARD_3:59;
then ( Rank (the_rank_of X) in Rank (card W) & X c= Rank (the_rank_of X) ) by CLASSES1:42, CLASSES1:def 8;
hence X in Rank (card W) by CLASSES1:47; :: thesis: verum