let T be TopSpace; (PSO T) /\ (D(c,ps) T) = the topology of T
thus
(PSO T) /\ (D(c,ps) T) c= the topology of T
XBOOLE_0:def 10 the topology of T c= (PSO T) /\ (D(c,ps) T)
let x be object ; TARSKI:def 3 ( not x in the topology of T or x in (PSO T) /\ (D(c,ps) T) )
assume A6:
x in the topology of T
; x in (PSO T) /\ (D(c,ps) T)
then reconsider K = x as Subset of T ;
A7:
Int (Cl K) c= Cl (Int (Cl K))
by PRE_TOPC:18;
K is open
by A6, PRE_TOPC:def 2;
then A8:
K = Int K
by TOPS_1:23;
then
K c= Int (Cl K)
by PRE_TOPC:18, TOPS_1:19;
then
K c= Cl (Int (Cl K))
by A7;
then A9:
K is pre-semi-open
;
then
Int K = psInt K
by A8, Th5;
then A10:
K in { B where B is Subset of T : Int B = psInt B }
;
K in PSO T
by A9;
hence
x in (PSO T) /\ (D(c,ps) T)
by A10, XBOOLE_0:def 4; verum