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