set EX = the TopSpace;
set C = the carrier of the TopSpace;
set T = the topology of the TopSpace;
set F = IntMap the TopSpace;
take TT = 2TopStruct(# the carrier of the TopSpace,(IntMap the TopSpace), the topology of the TopSpace #); :: thesis:
for x being object holds
( x in the topology of TT iff ex S being Subset of TT st
( S = x & S is op-open ) )

let x be object ; :: thesis:
thus ( x in the topology of TT implies ex S being Subset of TT st
( S = x & S is op-open ) ) :: thesis:

assume E1: x in the topology of TT ; :: thesis:
then reconsider X = x as Subset of TT ;
reconsider Y = X as Subset of the TopSpace ;
Int Y = Y by TOPS_1:23, E1, PRE_TOPC:def 2;
then X is op-open by ROUGHS_2:def 16;
hence ex S being Subset of TT st
( S = x & S is op-open ) ; :: thesis:

end;

assume ex S being Subset of TT st
( S = x & S is op-open ) ; :: thesis:
then consider S being Subset of TT such that
F1: ( S = x & S is op-open ) ;
reconsider SS = S as Subset of the TopSpace ;
Int SS = SS by F1, ROUGHS_2:def 16;
hence x in the topology of TT by F1, PRE_TOPC:def 2; :: thesis:

end;