:: deftheorem PDT defines with_properly_defined_topology ROUGHS_4:def 23 :
for T being 1TopStruct holds
( T is with_properly_defined_topology iff for x being object holds
( x in the topology of T iff ex S being Subset of T st
( S ` = x & S is op-closed ) ) );