let T be TopSpace; :: thesis: (PSO T) /\ (D(p,ps) T) = PO T
thus (PSO T) /\ (D(p,ps) T) c= PO T by XBOOLE_0:def 4; :: according to XBOOLE_0:def 10 :: thesis: PO T c= (PSO T) /\ (D(p,ps) T)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PO T or x in (PSO T) /\ (D(p,ps) T) )
assume x in PO T ; :: thesis: x in (PSO T) /\ (D(p,ps) T)
then consider K being Subset of T such that
A1: x = K and
A2: K is pre-open ;
A3: Int (Cl K) c= Cl (Int (Cl K)) by PRE_TOPC:18;
K c= Int (Cl K) by A2;
then K c= Cl (Int (Cl K)) by A3;
then A4: K is pre-semi-open ;
then K = psInt K by Th5;
then pInt K = psInt K by A2, Th4;
then A5: K in { B where B is Subset of T : pInt B = psInt B } ;
K in PSO T by A4;
hence x in (PSO T) /\ (D(p,ps) T) by A1, A5, XBOOLE_0:def 4; :: thesis: verum