A3: card W is limit_ordinal by A1, Th19;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Rank (card W) ; :: thesis:
then consider A being Ordinal such that
A4: A in card W and
A5: x in Rank A by A2, A3, CLASSES1:31;
A in On W by A1, A4, Th9;
then Rank A c= W by A1, Th7, Th25;
hence x in W by A5; :: thesis:

end;