let S be Subset of REAL; :: thesis: ( S is empty implies S is open )
assume S is empty ; :: thesis: S is open
then S ` = [#] REAL ;
hence S is open ; :: thesis: verum