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: ( TT is with_interior & TT is with_properly_defined_Topology )
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 ) )

proof

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

proof

assume E1: x in the topology of TT ; :: thesis: ex S being Subset of TT st
( S = x & S is op-open )
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: verum

end;

assume ex S being Subset of TT st
( S = x & S is op-open ) ; :: thesis: x in the topology of TT
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: verum

end;

hence ( TT is with_interior & TT is with_properly_defined_Topology ) ; :: thesis: verum