let T be TopSpace; (PO T) /\ (D(alpha,p) T) = T ^alpha
thus
(PO T) /\ (D(alpha,p) T) c= T ^alpha
XBOOLE_0:def 10 T ^alpha c= (PO T) /\ (D(alpha,p) T)
let x be object ; TARSKI:def 3 ( not x in T ^alpha or x in (PO T) /\ (D(alpha,p) T) )
assume
x in T ^alpha
; x in (PO T) /\ (D(alpha,p) 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;
K c= Int (Cl (Int K))
by A7, Def1;
then
K c= Int (Cl K)
by A8;
then A9:
K is pre-open
;
then
K = pInt K
by Th4;
then
alphaInt K = pInt K
by A7, Th2;
then A10:
K in { B where B is Subset of T : alphaInt B = pInt B }
;
K in PO T
by A9;
hence
x in (PO T) /\ (D(alpha,p) T)
by A6, A10, XBOOLE_0:def 4; verum