let T be with_properly_defined_topology 1TopStruct ; :: thesis: for A being Subset of T holds
( A is op-closed iff A is closed )
let A be Subset of T; :: thesis: ( A is op-closed iff A is closed )
set f = the FirstOp of T;
thus ( A is op-closed implies A is closed ) :: thesis: ( A is closed implies A is op-closed )
proof
assume A is op-closed ; :: thesis: A is closed
then A ` in the topology of T by PDT;
hence A is closed by TOPS_1:3, PRE_TOPC:def 2; :: thesis: verum
end;
thus ( A is closed implies A is op-closed ) :: thesis: verum
proof
assume A is closed ; :: thesis: A is op-closed
then A ` in the topology of T by PRE_TOPC:def 2, TOPS_1:3;
then consider S being Subset of T such that
K1: ( S ` = A ` & S is op-closed ) by PDT;
(S `) ` = (A `) ` by K1;
hence A is op-closed by K1; :: thesis: verum
end;