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

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