let n be Nat; :: thesis: for p being Point of (TOP-REAL n) st p in Sphere ((0. (TOP-REAL n)),1) holds
- p in (Sphere ((0. (TOP-REAL n)),1)) \ {p}
let p be Point of (TOP-REAL n); :: thesis: ( p in Sphere ((0. (TOP-REAL n)),1) implies - p in (Sphere ((0. (TOP-REAL n)),1)) \ {p} )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Point of (TOP-REAL n1) ;
assume p in Sphere ((0. (TOP-REAL n)),1) ; :: thesis: - p in (Sphere ((0. (TOP-REAL n)),1)) \ {p}
then |.(p1 - (0. (TOP-REAL n1))).| = 1 by TOPREAL9:9;
then |.(p1 + (- (0. (TOP-REAL n1)))).| = 1 ;
then |.(p + ((- 1) * (0. (TOP-REAL n)))).| = 1 by RLVECT_1:16;
then |.(p + (0. (TOP-REAL n))).| = 1 by RLVECT_1:10;
then A1: |.p.| = 1 by RLVECT_1:4;
reconsider r1 = 1 as Real ;
|.(0. (TOP-REAL n)).| <> |.p.| by A1, EUCLID_2:39;
then 0. (TOP-REAL n) <> (1 + 1) * p by RLVECT_1:11;
then 0. (TOP-REAL n) <> (r1 * p) + (r1 * p) by RLVECT_1:def 6;
then 0. (TOP-REAL n) <> (r1 * p) + p by RLVECT_1:def 8;
then 0. (TOP-REAL n) <> p + p by RLVECT_1:def 8;
then p + (- p) <> p + p by RLVECT_1:5;
then A2: not - p in {p} by TARSKI:def 1;
|.(- p).| = 1 by A1, EUCLID:71;
then |.((- p) + (0. (TOP-REAL n))).| = 1 by RLVECT_1:4;
then |.((- p) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by RLVECT_1:10;
then |.((- p) + (- (0. (TOP-REAL n)))).| = 1 by RLVECT_1:16;
then |.((- p1) - (0. (TOP-REAL n1))).| = 1 ;
then - p1 in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;
hence - p in (Sphere ((0. (TOP-REAL n)),1)) \ {p} by A2, XBOOLE_0:def 5; :: thesis: verum