let n be Nat; 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); ( 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)
; - 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; verum