let T be TopSpace; (PSO T) /\ (D(alpha,p) T) = SO T
thus
(PSO T) /\ (D(alpha,p) T) c= SO T
XBOOLE_0:def 10 SO T c= (PSO T) /\ (D(alpha,p) T)
let x be object ; TARSKI:def 3 ( not x in SO T or x in (PSO T) /\ (D(alpha,p) T) )
assume
x in SO T
; x in (PSO T) /\ (D(alpha,p) T)
then consider K being Subset of T such that
A1:
x = K
and
A2:
K is semi-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
Cl (Int K) c= Cl (Int (Cl K))
by TOPS_1:26;
then
K c= Cl (Int (Cl K))
by A2;
then A4:
K is pre-semi-open
;
then
K = psInt K
by Th5;
then
sInt K = psInt K
by A2, Th3;
then
alphaInt K = pInt K
by Th1;
then A5:
K in { B where B is Subset of T : alphaInt B = pInt B }
;
K in PSO T
by A4;
hence
x in (PSO T) /\ (D(alpha,p) T)
by A1, A5, XBOOLE_0:def 4; verum