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

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