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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (SO T) /\ (D(c,s) T) or x in the topology of T )
assume A1: x in (SO T) /\ (D(c,s) T) ; :: thesis: x in the topology of T
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(c,s) T by A1, XBOOLE_0:def 4;
then consider Z being Subset of T such that
A4: x = Z and
A5: Int Z = sInt Z ;
A = sInt A by A3, Th3;
then Z is open by A2, A4, A5, TOPS_1:51;
hence x in the topology of T by A4, 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 (SO T) /\ (D(c,s) T) )
assume A6: x in the topology of T ; :: thesis: x in (SO T) /\ (D(c,s) T)
then reconsider K = x as Subset of T ;
K is open by A6, PRE_TOPC:def 5;
then A7: K = Int K by TOPS_1:55;
then K c= Cl (Int K) by PRE_TOPC:48;
then A8: K is semi-open by Def2;
then Int K = sInt K by A7, Th3;
then A9: K in { B where B is Subset of T : Int B = sInt B } ;
K in SO T by A8;
hence x in (SO T) /\ (D(c,s) T) by A9, XBOOLE_0:def 4; :: thesis: verum