let r be non negative Real; :: 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:25;

n in NAT by ORDINAL1:def 12;

then A1: the carrier of (Tcircle ((0. (TOP-REAL n)),r)) = Sphere ((0. (TOP-REAL n)),r) by TOPREALB:9;

|.((- p1) - (0. (TOP-REAL n))).| = |.(- p1).|

.= |.p1.| by EUCLID:71

.= |.(p1 - (0. (TOP-REAL n))).|

.= r by A1, TOPREAL9:9 ;

hence - p is Point of (Tcircle ((0. (TOP-REAL n)),r)) by A1, TOPREAL9:9; :: thesis: verum

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:25;

n in NAT by ORDINAL1:def 12;

then A1: the carrier of (Tcircle ((0. (TOP-REAL n)),r)) = Sphere ((0. (TOP-REAL n)),r) by TOPREALB:9;

|.((- p1) - (0. (TOP-REAL n))).| = |.(- p1).|

.= |.p1.| by EUCLID:71

.= |.(p1 - (0. (TOP-REAL n))).|

.= r by A1, TOPREAL9:9 ;

hence - p is Point of (Tcircle ((0. (TOP-REAL n)),r)) by A1, TOPREAL9:9; :: thesis: verum