let F be Subset-Family of T; :: thesis: ( F is empty implies ( F is open & F is closed ) )
assume A1: F is empty ; :: thesis: ( F is open & F is closed )
then A2: 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 by A1;
hence ( F is open & F is closed ) by A2, TOPS_2:def 1, TOPS_2:def 2; :: thesis: verum