theorem :: CLASSES1:71

for X being set holds
( the_rank_of X = {} iff X = {} )