for T being with_properly_defined_Topology 2TopStruct
for A being Subset of T holds
( A is op-open iff A is open )