let r be real non negative number ; :: thesis: for n being non zero Nat
for p being Point of (Tcircle (0. (TOP-REAL n)),r) holds - p is Point of (Tcircle (0. (TOP-REAL n)),r)
let n be non zero Nat; :: thesis: for p being Point of (Tcircle (0. (TOP-REAL n)),r) holds - p is Point of (Tcircle (0. (TOP-REAL n)),r)
let p be Point of (Tcircle (0. (TOP-REAL n)),r); :: thesis: - p is Point of (Tcircle (0. (TOP-REAL n)),r)
reconsider p1 = p as Point of (TOP-REAL n) by PRE_TOPC:55;
A1: n in NAT by ORDINAL1:def 13;
then A2: the carrier of (Tcircle (0. (TOP-REAL n)),r) = Sphere (0. (TOP-REAL n)),r by TOPREALB:9;
|.((- p1) - (0. (TOP-REAL n))).| = |.(- p1).| by RLVECT_1:26
.= |.p1.| by EUCLID:75
.= |.(p1 - (0. (TOP-REAL n))).| by RLVECT_1:26
.= r by A1, A2, TOPREAL9:9 ;
hence - p is Point of (Tcircle (0. (TOP-REAL n)),r) by A2, A1, TOPREAL9:9; :: thesis: verum