let S be Subset of T; :: thesis: ( S is empty implies S is open )
Int ({} T) = {} T ;
hence ( S is empty implies S is open ) ; :: thesis: verum