let n be Nat; :: thesis: for O1 being Subset of (TOP-REAL n)
for O2 being Subset of (TopSpaceMetr (Euclid n)) st O1 = O2 holds
( O1 is open iff O2 is open )
let O1 be Subset of (TOP-REAL n); :: thesis: for O2 being Subset of (TopSpaceMetr (Euclid n)) st O1 = O2 holds
( O1 is open iff O2 is open )
let O2 be Subset of (TopSpaceMetr (Euclid n)); :: thesis: ( O1 = O2 implies ( O1 is open iff O2 is open ) )
assume A1: O1 = O2 ; :: thesis: ( O1 is open iff O2 is open )
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
hence ( O1 is open iff O2 is open ) by A1; :: thesis: verum