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