set EX = the TopSpace;
set C = the carrier of the TopSpace;
set T = the topology of the TopSpace;
set F = ClMap the TopSpace;
take TT = 1TopStruct(# the carrier of the TopSpace,(ClMap the TopSpace), the topology of the TopSpace #); :: thesis: ( TT is with_closure & 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-closed ) )

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-closed ) )
thus ( x in the topology of TT implies ex S being Subset of TT st
( S ` = x & S is op-closed ) ) :: thesis: ( ex S being Subset of TT st
( S ` = x & S is op-closed ) 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-closed )
then reconsider X = x as Subset of TT ;
reconsider Y = X as Subset of the TopSpace ;
Y is open by E1, PRE_TOPC:def 2;
then Cl (Y `) = Y ` by PRE_TOPC:22;
then E5: X ` is op-closed by ROUGHS_2:def 15;
(X `) ` = x ;
hence ex S being Subset of TT st
( S ` = x & S is op-closed ) by E5; :: thesis: verum

end;

assume ex S being Subset of TT st
( S ` = x & S is op-closed ) ; :: thesis: x in the topology of TT
then consider S being Subset of TT such that
F1: ( S ` = x & S is op-closed ) ;
reconsider SS = S as Subset of the TopSpace ;
(ClMap the TopSpace) . SS = Cl SS by ROUGHS_2:def 15;
hence x in the topology of TT by F1, PRE_TOPC:def 2; :: thesis: verum

end;

hence ( TT is with_closure & TT is with_properly_defined_topology ) ; :: thesis: verum