:: deftheorem PDTo defines with_properly_defined_Topology ROUGHS_4:def 24 :
for T being 2TopStruct 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-open ) ) );