let m be non empty Element of NAT ; :: thesis: for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X = Y holds
( X is open iff Y is open )
let X be Subset of (REAL m); :: thesis: for Y being Subset of (REAL-NS m) st X = Y holds
( X is open iff Y is open )
let Y be Subset of (REAL-NS m); :: thesis: ( X = Y implies ( X is open iff Y is open ) )
assume A1: X = Y ; :: thesis: ( X is open iff Y is open )

hereby :: thesis: ( Y is open implies X is open )

assume X is open ; :: thesis: Y is open
then ex X0 being Subset of (REAL-NS m) st
( X0 = X & X0 is open ) by PDIFF_7:def 3;
hence Y is open by A1; :: thesis: verum

end;

thus ( Y is open implies X is open ) by A1, PDIFF_7:def 3; :: thesis: verum