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)) )_{1} being Subset of (Tcircle ((0. (TOP-REAL (m + 1))),r)) st b_{1} = (-) X holds

b_{1} is open
by TSP_1:def 1; :: thesis: verum

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

hence
for b
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

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;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 ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) or x in (-) X )
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;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

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

b