let n be non empty Element of NAT ; :: thesis: for r, s being real positive number
for x, y being Point of (TOP-REAL n) holds Tcircle x,r, Tcircle y,s are_homeomorphic
let r, s be real positive number ; :: thesis: for x, y being Point of (TOP-REAL n) holds Tcircle x,r, Tcircle y,s are_homeomorphic
let x, y be Point of (TOP-REAL n); :: thesis: Tcircle x,r, Tcircle y,s are_homeomorphic
A1: Tunit_circle n, Tcircle y,s are_homeomorphic by Lm14;
Tcircle x,r, Tunit_circle n are_homeomorphic by Lm14;
hence Tcircle x,r, Tcircle y,s are_homeomorphic by A1, BORSUK_3:3; :: thesis: verum