let F be Subset-Family of T; :: thesis: ( F is empty implies ( F is open & F is closed ) )
assume F is empty ; :: thesis: ( F is open & F is closed )
then ( ( for P being Subset of T st P in F holds
P is open ) & ( for P being Subset of T st P in F holds
P is closed ) ) ;
hence ( F is open & F is closed ) by TOPS_2:def 1, TOPS_2:def 2; :: thesis: verum