let U be Point of (TOP-REAL 1); for r, u1 being Real st <*u1*> = U & r > 0 holds
Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
let r, u1 be Real; ( <*u1*> = U & r > 0 implies Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} )
assume that
A1:
<*u1*> = U
and
A2:
r > 0
; Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
reconsider u = U as Point of (Euclid 1) by Lm6;
A3:
Ball (u,r) = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) }
by A1, JORDAN2B:27;
Ball (U,r) = Ball (u,r)
by TOPREAL9:13;
then
Ball (U,r) is open
by KURATO_2:1;
then A4: Fr (Ball (U,r)) =
(Cl (Ball (U,r))) \ (Ball (U,r))
by TOPS_1:42
.=
(cl_Ball (U,r)) \ (Ball (U,r))
by A2, JORDAN:23
.=
(cl_Ball (u,r)) \ (Ball (U,r))
by TOPREAL9:14
.=
(cl_Ball (u,r)) \ (Ball (u,r))
by TOPREAL9:13
;
A5:
cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) }
by A1, Th17;
thus
Fr (Ball (U,r)) c= {<*(u1 - r)*>,<*(u1 + r)*>}
XBOOLE_0:def 10 {<*(u1 - r)*>,<*(u1 + r)*>} c= Fr (Ball (U,r))proof
let x be
object ;
TARSKI:def 3 ( not x in Fr (Ball (U,r)) or x in {<*(u1 - r)*>,<*(u1 + r)*>} )
assume A6:
x in Fr (Ball (U,r))
;
x in {<*(u1 - r)*>,<*(u1 + r)*>}
reconsider X =
x as
Point of
(Euclid 1) by Lm6, A6;
x in cl_Ball (
u,
r)
by A4, A6, XBOOLE_0:def 5;
then consider s being
Real such that A7:
x = <*s*>
and A8:
u1 - r <= s
and A9:
s <= u1 + r
by A5;
assume A10:
not
x in {<*(u1 - r)*>,<*(u1 + r)*>}
;
contradiction
then
s <> u1 + r
by A7, TARSKI:def 2;
then A11:
s < u1 + r
by A9, XXREAL_0:1;
s <> u1 - r
by A7, A10, TARSKI:def 2;
then
u1 - r < s
by A8, XXREAL_0:1;
then
X in Ball (
u,
r)
by A3, A7, A11;
hence
contradiction
by A4, A6, XBOOLE_0:def 5;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {<*(u1 - r)*>,<*(u1 + r)*>} or x in Fr (Ball (U,r)) )
assume
x in {<*(u1 - r)*>,<*(u1 + r)*>}
; x in Fr (Ball (U,r))
then A12:
( x = <*(u1 - r)*> or x = <*(u1 + r)*> )
by TARSKI:def 2;
assume A13:
not x in Fr (Ball (U,r))
; contradiction
u1 + (- r) <= u1 + r
by A2, XREAL_1:6;
then
x in cl_Ball (u,r)
by A5, A12;
then
x in Ball (u,r)
by A4, A13, XBOOLE_0:def 5;
then
ex s being Real st
( x = <*s*> & u1 - r < s & s < u1 + r )
by A3;
hence
contradiction
by A12, FINSEQ_1:76; verum