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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (PSO T) /\ (D(sp,ps) T) or x in SPO T )
assume x in (PSO T) /\ (D(sp,ps) T) ; :: thesis: x in SPO T
then A0: ( x in PSO T & x in D(sp,ps) T ) by XBOOLE_0:def 4;
then consider B being Subset of T such that
A1: ( x = B & B is pre-semi-open ) ;
A3: B = psInt B by A1, Th5;
consider B1 being Subset of T such that
A2: ( x = B1 & spInt B1 = psInt B1 ) by A0;
B is semi-pre-open by A1, A2, A3, Th6;
hence x in SPO T by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SPO T or x in (PSO T) /\ (D(sp,ps) T) )
assume x in SPO T ; :: thesis: x in (PSO T) /\ (D(sp,ps) T)
then consider K being Subset of T such that
A1: x = K and
A2: K is semi-pre-open ;
Cl (Int K) c= Cl K by PRE_TOPC:19, TOPS_1:16;
then Int (Cl (Int K)) c= Int (Cl K) by TOPS_1:19;
then Cl (Int (Cl (Int K))) c= Cl (Int (Cl K)) by PRE_TOPC:19;
then A3: Cl (Int K) c= Cl (Int (Cl K)) by TOPS_1:26;
Int (Cl K) c= Cl (Int (Cl K)) by PRE_TOPC:18;
then (Cl (Int K)) \/ (Int (Cl K)) c= Cl (Int (Cl K)) by A3, XBOOLE_1:8;
then K c= Cl (Int (Cl K)) by A2;
then A5: K is pre-semi-open ;
then K = psInt K by Th5;
then spInt K = psInt K by A2, Th6;
then A6: K in { B where B is Subset of T : spInt B = psInt B } ;
K in PSO T by A5;
hence x in (PSO T) /\ (D(sp,ps) T) by A1, A6, XBOOLE_0:def 4; :: thesis: verum