let T be TopSpace; (PSO T) /\ (D(alpha,ps) T) = T ^alpha
thus
(PSO T) /\ (D(alpha,ps) T) c= T ^alpha
XBOOLE_0:def 10 T ^alpha c= (PSO T) /\ (D(alpha,ps) T)
let x be object ; TARSKI:def 3 ( not x in T ^alpha or x in (PSO T) /\ (D(alpha,ps) T) )
assume
x in T ^alpha
; x in (PSO T) /\ (D(alpha,ps) T)
then consider K being Subset of T such that
A6:
x = K
and
A7:
K is alpha-set of T
;
Cl (Int K) c= Cl K
by PRE_TOPC:19, TOPS_1:16;
then A8:
Int (Cl (Int K)) c= Int (Cl K)
by TOPS_1:19;
Int (Cl K) c= Cl (Int (Cl K))
by PRE_TOPC:18;
then A9:
Int (Cl (Int K)) c= Cl (Int (Cl K))
by A8;
K c= Int (Cl (Int K))
by A7, Def1;
then
K c= Cl (Int (Cl K))
by A9;
then A10:
K is pre-semi-open
;
then
K = psInt K
by Th5;
then
alphaInt K = psInt K
by A7, Th2;
then A11:
K in { B where B is Subset of T : alphaInt B = psInt B }
;
K in PSO T
by A10;
hence
x in (PSO T) /\ (D(alpha,ps) T)
by A6, A11, XBOOLE_0:def 4; verum