let S be Subset of T; :: thesis: ( S is empty implies ( S is regular_open & S is regular_closed ) )
assume A1: S is empty ; :: thesis: ( S is regular_open & S is regular_closed )
then A2: S = Int S ;
S = Cl S by A1, PCOMPS_1:2;
hence ( S is regular_open & S is regular_closed ) by A2, TOPS_1:def 7, TOPS_1:def 8; :: thesis: verum