let n be Nat; :: thesis: for p, q being Point of (TOP-REAL (n + 1)) st p <> 0. (TOP-REAL (n + 1)) holds
TOP-REAL n, TPlane (p,q) are_homeomorphic
set T1 = TOP-REAL (n + 1);
let p, q be Point of (TOP-REAL (n + 1)); :: thesis: ( p <> 0. (TOP-REAL (n + 1)) implies TOP-REAL n, TPlane (p,q) are_homeomorphic )
assume A1: p <> 0. (TOP-REAL (n + 1)) ; :: thesis: TOP-REAL n, TPlane (p,q) are_homeomorphic
reconsider p0 = Base_FinSeq ((n + 1),(n + 1)) as Point of (TOP-REAL (n + 1)) by EUCLID:22;
A2: p0 <> 0. (TOP-REAL (n + 1))
proof
assume A3: p0 = 0. (TOP-REAL (n + 1)) ; :: thesis: contradiction
0 + 1 <= n + 1 by XREAL_1:6;
then |.p0.| = 1 by EUCLID_7:28;
hence contradiction by A3, EUCLID_2:39; :: thesis: verum
end;
A4: TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic by Lm3;
ex R being Function of (TOP-REAL (n + 1)),(TOP-REAL (n + 1)) st
( R is being_homeomorphism & R .: (Plane (p0,(0. (TOP-REAL (n + 1))))) = Plane (p,(0. (TOP-REAL (n + 1)))) ) by A1, A2, Th27;
then TPlane (p0,(0. (TOP-REAL (n + 1)))), TPlane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by METRIZTS:3, METRIZTS:def 1;
then A5: TOP-REAL n, TPlane (p,(0. (TOP-REAL (n + 1)))) are_homeomorphic by A4, BORSUK_3:3;
(transl (q,(TOP-REAL (n + 1)))) .: (Plane (p,(0. (TOP-REAL (n + 1))))) = Plane (p,((0. (TOP-REAL (n + 1))) + q)) by Th25
.= Plane (p,q) by RLVECT_1:4 ;
then (TOP-REAL (n + 1)) | (Plane (p,(0. (TOP-REAL (n + 1))))),(TOP-REAL (n + 1)) | (Plane (p,q)) are_homeomorphic by METRIZTS:3, METRIZTS:def 1;
hence TOP-REAL n, TPlane (p,q) are_homeomorphic by A5, BORSUK_3:3; :: thesis: verum