let W be set ; :: thesis: ( W is Tarski implies card W = card (Rank (card W)) )
assume W is Tarski ; :: thesis: card W = card (Rank (card W))
then A1: card (Rank (card W)) c= card W by Th27, CARD_1:11;
card (card W) c= card (Rank (card W)) by CARD_1:11, CLASSES1:38;
hence card W = card (Rank (card W)) by A1; :: thesis: verum