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 that
A1: W is Tarski and
A2: A in On W ; :: thesis: card (Rank A) c= card W
card (Rank A) in card W by A1, A2, Th25;
hence card (Rank A) c= card W by CARD_1:3; :: thesis: verum