let A be Ordinal; :: thesis: for W being set st W is Tarski & A in On W holds
( card (Rank A) in card W & Rank A in W )
let W be set ; :: thesis: ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) )
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(Lm2, Lm3, Lm4);
hence ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) ) ; :: thesis: verum