let S be Subset of REAL; :: thesis: ( S is empty implies S is closed )
assume A1: 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 that
A2: rng a c= S and
a is convergent ; :: thesis: lim a in S
thus lim a in S by A1, A2, XBOOLE_1:3; :: thesis: verum