let S be Subset of REAL ; :: thesis: ( S is empty implies S is closed )
assume Z: S is empty ; :: thesis: S is closed
let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not rng a c= S or not a is convergent or lim a in S )
assume ( rng a c= S & a is convergent ) ; :: thesis: lim a in S
then rng a = S by Z, XBOOLE_1:3;
then dom a = S by Z;
hence lim a in S by Z; :: thesis: verum