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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (SO T) /\ (D(alpha,s) T) or x in T ^alpha )
assume A1: x in (SO T) /\ (D(alpha,s) T) ; :: thesis: x in T ^alpha
then x in SO T by XBOOLE_0:def 4;
then consider A being Subset of T such that
A2: x = A and
A3: A is semi-open ;
x in D(alpha,s) T by A1, XBOOLE_0:def 4;
then consider Z being Subset of T such that
A4: x = Z and
A5: alphaInt Z = sInt Z ;
Z is alpha-set of T by A2, A4, A5, Th2, A3, Th3;
hence x in T ^alpha by A4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T ^alpha or x in (SO T) /\ (D(alpha,s) T) )
assume x in T ^alpha ; :: thesis: x in (SO T) /\ (D(alpha,s) T)
then consider K being Subset of T such that
A6: x = K and
A7: K is alpha-set of T ;
A8: Int (Cl (Int K)) c= Cl (Int K) by TOPS_1:16;
K c= Int (Cl (Int K)) by A7, Def1;
then K c= Cl (Int K) by A8;
then A9: K is semi-open ;
then K = sInt K by Th3;
then alphaInt K = sInt K by A7, Th2;
then A10: K in { B where B is Subset of T : alphaInt B = sInt B } ;
K in { B where B is Subset of T : B is semi-open } by A9;
hence x in (SO T) /\ (D(alpha,s) T) by A6, A10, XBOOLE_0:def 4; :: thesis: verum