let A be Ordinal; :: thesis: for W being set st W is Tarski & A in On W holds
card (Rank A) c= card W
let W be set ; :: thesis: ( W is Tarski & A in On W implies card (Rank A) c= card W )
assume ( W is Tarski & A in On W ) ; :: thesis: card (Rank A) c= card W
then card (Rank A) in card W by Th26;
hence card (Rank A) c= card W by CARD_1:13; :: thesis: verum