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))

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

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

A4:
TOP-REAL n, TPlane (p0,(0. (TOP-REAL (n + 1)))) are_homeomorphic
by Lm3;
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;0 + 1 <= n + 1 by XREAL_1:6;

then |.p0.| = 1 by EUCLID_7:28;

hence contradiction by A3, EUCLID_2:39; :: thesis: verum

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