theorem Th62: :: CLASSES2:62

card (Rank omega) = card omega