for T being with_closure with_properly_defined_topology 1TopStruct
for A being Subset of T holds the FirstOp of T . A = Cl A