let A be Ordinal; :: thesis: for W being set st A in On (Tarski-Class W) holds
card (Rank A) c= card (Tarski-Class W)
let W be set ; :: thesis: ( A in On (Tarski-Class W) implies card (Rank A) c= card (Tarski-Class W) )
assume A in On (Tarski-Class W) ; :: thesis: card (Rank A) c= card (Tarski-Class W)
then card (Rank A) in card (Tarski-Class W) by Th25;
hence card (Rank A) c= card (Tarski-Class W) by CARD_1:3; :: thesis: verum