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
;
( (-) G is open & (-) X = ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) )
thus
(-) G is
open
by A1;
(-) 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))
XBOOLE_0:def 10 ((-) G) /\ the carrier of (Tcircle ((0. (TOP-REAL (m + 1))),r)) c= (-) X
let x be
object ;
TARSKI:def 3 ( 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))
;
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;
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; verum