theorem Lem1: :: ROUGHS_4:2

for T being with_properly_defined_topology 1TopStruct
for A being Subset of T holds
( A is op-closed iff A is closed )