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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (PO T) /\ (D(alpha,p) T) or x in T ^alpha )
assume x in (PO T) /\ (D(alpha,p) T) ; :: thesis: x in T ^alpha
then A1: ( x in PO T & x in D(alpha,p) T ) by XBOOLE_0:def 4;
then consider A being Subset of T such that
A2: x = A and
A3: A is pre-open ;
A4: A = pInt A by A3, Th4;
consider Z being Subset of T such that
A5: x = Z and
A6: alphaInt Z = pInt Z by A1;
Z is alpha-set of T by A2, A4, A5, A6, Th2;
hence x in T ^alpha by A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T ^alpha or x in (PO T) /\ (D(alpha,p) T) )
assume x in T ^alpha ; :: thesis: x in (PO T) /\ (D(alpha,p) T)
then consider K being Subset of T such that
A7: x = K and
A8: K is alpha-set of T ;
A9: K c= Int (Cl (Int K)) by A8, Def1;
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 K c= Int (Cl K) by A9, XBOOLE_1:1;
then A10: K is pre-open by Def3;
then A11: K = pInt K by Th4;
A12: K in PO T by A10;
alphaInt K = pInt K by A8, A11, Th2;
then K in { B where B is Subset of T : alphaInt B = pInt B } ;
hence x in (PO T) /\ (D(alpha,p) T) by A7, A12, XBOOLE_0:def 4; :: thesis: verum