let T be with_properly_defined_Topology 2TopStruct ; :: thesis: for A being Subset of T holds
( A is op-open iff A is open )
let A be Subset of T; :: thesis: ( A is op-open iff A is open )
set f = the SecondOp of T;
thus ( A is op-open implies A is open ) :: thesis: ( A is open implies A is op-open )
proof
assume A is op-open ; :: thesis: A is open
then A in the topology of T by PDTo;
hence A is open by PRE_TOPC:def 2; :: thesis: verum
end;
assume A is open ; :: thesis: A is op-open
then A in the topology of T by PRE_TOPC:def 2;
then ex S being Subset of T st
( S = A & S is op-open ) by PDTo;
hence A is op-open ; :: thesis: verum