set T = Tcircle ((0. (TOP-REAL (n + 1))),r);
(-) X c= the carrier of (Tcircle ((0. (TOP-REAL (n + 1))),r))
proof
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;
hence (-) X is Subset of (Tcircle ((0. (TOP-REAL (n + 1))),r)) ; :: thesis: verum