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 A1: the_rank_of X = {} ; :: thesis: X = {}
A2: X c= Rank {} by A1, Def8;
thus X = {} by A2, Lm2; :: thesis: verum

end;

assume A3: X = {} ; :: thesis: the_rank_of X = {}
A4: for Y being set st Y in X holds
the_rank_of Y in {} by A3;
thus the_rank_of X c= {} by A4, Th77; :: according to XBOOLE_0:def 10 :: thesis: {} c= the_rank_of X
thus {} c= the_rank_of X ; :: thesis: verum