let n be non zero Element of NAT ; :: thesis: for r, s being positive Real
for x, y being Point of (TOP-REAL n) holds Tcircle (x,r), Tcircle (y,s) are_homeomorphic
let r, s be positive Real; :: 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