let T be TopSpace; :: thesis: (SPO T) /\ (D(p,sp) T) = PO T
thus (SPO T) /\ (D(p,sp) T) c= PO T :: according to XBOOLE_0:def 10 :: thesis: PO T c= (SPO T) /\ (D(p,sp) T)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (SPO T) /\ (D(p,sp) T) or x in PO T )
assume A1: x in (SPO T) /\ (D(p,sp) T) ; :: thesis: x in PO T
then x in SPO T by XBOOLE_0:def 4;
then consider A being Subset of T such that
A2: x = A and
A3: A is semi-pre-open ;
x in D(p,sp) T by A1, XBOOLE_0:def 4;
then consider Z being Subset of T such that
A4: x = Z and
A5: pInt Z = spInt Z ;
A = spInt A by A3, Th6;
then Z is pre-open by A2, A4, A5, Th4;
hence x in PO T by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PO T or x in (SPO T) /\ (D(p,sp) T) )
assume x in PO T ; :: thesis: x in (SPO T) /\ (D(p,sp) T)
then consider K being Subset of T such that
A6: x = K and
A7: K is pre-open ;
A8: Int (Cl K) c= (Cl (Int K)) \/ (Int (Cl K)) by XBOOLE_1:7;
K c= Int (Cl K) by A7, Def3;
then K c= (Cl (Int K)) \/ (Int (Cl K)) by A8, XBOOLE_1:1;
then A9: K is semi-pre-open by Def5;
then K = spInt K by Th6;
then pInt K = spInt K by A7, Th4;
then A10: K in { B where B is Subset of T : pInt B = spInt B } ;
K in SPO T by A9;
hence x in (SPO T) /\ (D(p,sp) T) by A6, A10, XBOOLE_0:def 4; :: thesis: verum