let X, W 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, Th41, ORDINAL1:12;
card (card W) = card W ;
then the_rank_of X in card W by A3, CARD_3:43;
then A4: Rank (the_rank_of X) in Rank (card W) by CLASSES1:36;
X c= Rank (the_rank_of X) by CLASSES1:def 9;
hence X in Rank (card W) by A4, CLASSES1:41; :: thesis: verum