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 Th28, CARD_1:27;
( card (card W) = card W & card (card W) c= card (Rank (card W)) ) by CARD_1:27, CLASSES1:44;
hence card W = card (Rank (card W)) by A1, XBOOLE_0:def 10; :: thesis: verum