let T be TopSpace; :: thesis: (PSO T) /\ (D(alpha,p) T) = SO T
thus (PSO T) /\ (D(alpha,p) T) c= SO T :: according to XBOOLE_0:def 10 :: thesis: SO T c= (PSO T) /\ (D(alpha,p) T)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (PSO T) /\ (D(alpha,p) T) or x in SO T )
assume A1: x in (PSO T) /\ (D(alpha,p) T) ; :: thesis: x in SO T
then x in PSO T by XBOOLE_0:def 4;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-semi-open ;
x in D(alpha,p) T by A1, XBOOLE_0:def 4;
then consider Z being Subset of T such that
A4: x = Z and
A5: alphaInt Z = pInt Z ;
A = psInt A by A3, Th5;
then Z = sInt Z by A2, A4, A5, Th1;
then Z is semi-open by Th3;
hence x in SO T by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SO T or x in (PSO T) /\ (D(alpha,p) T) )
assume x in SO T ; :: thesis: x in (PSO T) /\ (D(alpha,p) T)
then consider K being Subset of T such that
A6: x = K and
A7: K is semi-open ;
Cl (Int K) c= Cl K by PRE_TOPC:49, TOPS_1:44;
then Int (Cl (Int K)) c= Int (Cl K) by TOPS_1:48;
then Cl (Int (Cl (Int K))) c= Cl (Int (Cl K)) by PRE_TOPC:49;
then A8: Cl (Int K) c= Cl (Int (Cl K)) by TOPS_1:58;
K c= Cl (Int K) by A7, Def2;
then K c= Cl (Int (Cl K)) by A8, XBOOLE_1:1;
then A9: K is pre-semi-open by Def4;
then K = psInt K by Th5;
then sInt K = psInt K by A7, Th3;
then alphaInt K = pInt K by Th1;
then A10: K in { B where B is Subset of T : alphaInt B = pInt B } ;
K in PSO T by A9;
hence x in (PSO T) /\ (D(alpha,p) T) by A6, A10, XBOOLE_0:def 4; :: thesis: verum