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 by EUCLID:41;
then |.(p + ((- 1) * (0. (TOP-REAL n)))).| = 1 by EUCLID:39;
then |.(p + (0. (TOP-REAL n))).| = 1 by EUCLID:28;
then A1: |.p.| = 1 by EUCLID:27;
reconsider r1 = 1 as real number ;
|.(0. (TOP-REAL n)).| <> |.p.| by A1, EUCLID_2:39;
then 0. (TOP-REAL n) <> (1 + 1) * p by EUCLID:31;
then 0. (TOP-REAL n) <> (r1 * p) + (r1 * p) by EUCLID:33;
then 0. (TOP-REAL n) <> (r1 * p) + p by EUCLID:29;
then 0. (TOP-REAL n) <> p + p by EUCLID:29;
then p + (- p) <> p + p by EUCLID:36;
then A2: not - p in {p} by TARSKI:def 1;
|.(- p).| = 1 by A1, EUCLID:71;
then |.((- p) + (0. (TOP-REAL n))).| = 1 by EUCLID:27;
then |.((- p) + ((- 1) * (0. (TOP-REAL n)))).| = 1 by EUCLID:28;
then |.((- p) + (- (0. (TOP-REAL n)))).| = 1 by EUCLID:39;
then |.((- p1) - (0. (TOP-REAL n1))).| = 1 by EUCLID:41;
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