theorem Th41: :: CLASSES2:41

for X being set st X is epsilon-transitive holds
card (the_rank_of X) c= card X