set T = Tcircle ((0. (TOP-REAL (m + 1))),r);
ex G being Subset of (TOP-REAL (m + 1)) st
( G is open & (-) X = G /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
proof
consider G being Subset of (TOP-REAL (m + 1)) such that
A1: G is open and
A2: X = G /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by TSP_1:def 1;
take (-) G ; :: thesis: ( (-) G is open & (-) X = ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
thus (-) G is open by A1; :: thesis: (-) X = ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r))
thus (-) X c= ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) :: according to XBOOLE_0:def 10 :: thesis: ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) c= (-) X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (-) X or x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
assume A3: x in (-) X ; :: thesis: x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r))
then reconsider x = x as Element of (-) X ;
- x in X by A3, Th24;
then - x in G by A2, XBOOLE_0:def 4;
then x in (-) G by Th24;
hence x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by A3, XBOOLE_0:def 4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) or x in (-) X )
assume A4: x in ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) ; :: thesis: x in (-) X
then reconsider x = x as Element of (-) G by XBOOLE_0:def 4;
x in (-) G by A4, XBOOLE_0:def 4;
then A5: - x in G by Th24;
x in the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by A4, XBOOLE_0:def 4;
then - x is Point of (Tcircle ((0. (TOP-REAL (m + 1))),r)) by Th60;
then - x in X by A2, A5, XBOOLE_0:def 4;
hence x in (-) X by Th24; :: thesis: verum
end;
hence for b1 being Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st b1 = (-) X holds
b1 is open by TSP_1:def 1; :: thesis: verum