let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
A2,A1 are_homeomorphic
let A1 be Subset of T1; :: thesis: for A2 being Subset of T2 st A1,A2 are_homeomorphic holds
A2,A1 are_homeomorphic
let A2 be Subset of T2; :: thesis: ( A1,A2 are_homeomorphic implies A2,A1 are_homeomorphic )
assume A1,A2 are_homeomorphic ; :: thesis: A2,A1 are_homeomorphic
then T1 | A1,T2 | A2 are_homeomorphic by METRIZTS:def 1;
hence A2,A1 are_homeomorphic by METRIZTS:def 1; :: thesis: verum