let A be Subset of TS; :: thesis: ( A is empty implies ( A is open & A is closed ) )
assume A is empty ; :: thesis: ( A is open & A is closed )
then A = {} TS ;
hence ( A is open & A is closed ) ; :: thesis: verum