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

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of T or x in (T ^alpha ) /\ (D(c,alpha) T) )
assume A7: x in the topology of T ; :: thesis: x in (T ^alpha ) /\ (D(c,alpha) T)
then reconsider K = x as Subset of T ;
K is open by A7, PRE_TOPC:def 5;
then A8: K = Int K by TOPS_1:55;
then K c= Int (Cl (Int K)) by PRE_TOPC:48, TOPS_1:48;
then A9: K is alpha-set of T by Def1;
then A10: K in T ^alpha ;
Int K = alphaInt K by A8, A9, Th2;
then K in { B where B is Subset of T : Int B = alphaInt B } ;
hence x in (T ^alpha ) /\ (D(c,alpha) T) by A10, XBOOLE_0:def 4; :: thesis: verum