let X be set ; :: thesis: ( the_rank_of X = {} iff X = {} )
thus ( the_rank_of X = {} implies X = {} ) :: thesis: ( X = {} implies the_rank_of X = {} )

proof

assume the_rank_of X = {} ; :: thesis: X = {}
then X c= Rank {} by Def9;
hence X = {} by Lm2; :: thesis: verum

end;

assume X = {} ; :: thesis: the_rank_of X = {}
then for Y being set st Y in X holds
the_rank_of Y in {} ;
hence the_rank_of X c= {} by Th69; :: according to XBOOLE_0:def 10 :: thesis: {} c= the_rank_of X
thus {} c= the_rank_of X ; :: thesis: verum