theorem Th9: :: CLASSES2:9

for W being set st W is Tarski holds
On W = card W