let A be Subset of REAL; :: thesis: for B being Subset of R^1 st A = B holds
( A is open iff B is open )
let B be Subset of R^1; :: thesis: ( A = B implies ( A is open iff B is open ) )
assume A1: A = B ; :: thesis: ( A is open iff B is open )
hereby :: thesis: ( B is open implies A is open )
assume A is open ; :: thesis: B is open
then A in Family_open_set RealSpace by JORDAN5A:5;
then A in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12;
hence B is open by A1, PRE_TOPC:def 2, TOPMETR:def 6; :: thesis: verum
end;
assume B is open ; :: thesis: A is open
then B in the topology of R^1 by PRE_TOPC:def 2;
then A in Family_open_set RealSpace by A1, TOPMETR:12, TOPMETR:def 6;
hence A is open by JORDAN5A:5; :: thesis: verum