set T = Tcircle ((0. (TOP-REAL (n + 1))),r);

(-) X c= the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))

(-) X c= the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))

proof

hence
(-) X is Subset of (Tcircle ((0. (TOP-REAL (n + 1))),r))
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (-) X or x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) )

assume A1: x in (-) X ; :: thesis: x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))

then reconsider x = x as Element of (-) X ;

- x in X by A1, Th24;

then - (- x) is Point of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by Th60;

hence x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; :: thesis: verum

end;assume A1: x in (-) X ; :: thesis: x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))

then reconsider x = x as Element of (-) X ;

- x in X by A1, Th24;

then - (- x) is Point of (Tcircle ((0. (TOP-REAL (n + 1))),r)) by Th60;

hence x in the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; :: thesis: verum