let W be set ; :: thesis: Rank (card (Tarski-Class W)) c= Tarski-Class W
A1: card (Tarski-Class W) is limit_ordinal by Th21;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Rank (card (Tarski-Class W)) or x in Tarski-Class W )
assume x in Rank (card (Tarski-Class W)) ; :: thesis: x in Tarski-Class W
then consider A being Ordinal such that
A2: A in card (Tarski-Class W) and
A3: x in Rank A by A1, CLASSES1:31;
A in On (Tarski-Class W) by A2, Th9;
then Rank A c= Tarski-Class W by Th7, Th25;
hence x in Tarski-Class W by A3; :: thesis: verum