let U be Point of (TOP-REAL 1); :: thesis: for u1, r being real number st <*u1*> = U & r > 0 holds
Fr (Ball U,r) = {<*(u1 - r)*>,<*(u1 + r)*>}
let u1, r be real number ; :: thesis: ( <*u1*> = U & r > 0 implies Fr (Ball U,r) = {<*(u1 - r)*>,<*(u1 + r)*>} )
assume that
A1: <*u1*> = U and
A2: r > 0 ; :: thesis: Fr (Ball U,r) = {<*(u1 - r)*>,<*(u1 + r)*>}
reconsider u = U as Point of (Euclid 1) by A;
A3: Ball u,r = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } by A1, A2, JORDAN2B:33;
Ball U,r = Ball u,r by TOPREAL9:13;
then Ball U,r is open by KURATO_2:30;
then A4: Fr (Ball U,r) = (Cl (Ball U,r)) \ (Ball U,r) by TOPS_1:76
.= (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, A2, Th17;
thus Fr (Ball U,r) c= {<*(u1 - r)*>,<*(u1 + r)*>} :: according to XBOOLE_0:def 10 :: thesis: {<*(u1 - r)*>,<*(u1 + r)*>} c= Fr (Ball U,r)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (Ball U,r) or x in {<*(u1 - r)*>,<*(u1 + r)*>} )
assume A6: x in Fr (Ball U,r) ; :: thesis: x in {<*(u1 - r)*>,<*(u1 + r)*>}
reconsider X = x as Point of (Euclid 1) by A, 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)*>} ; :: thesis: 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; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*(u1 - r)*>,<*(u1 + r)*>} or x in Fr (Ball U,r) )
assume x in {<*(u1 - r)*>,<*(u1 + r)*>} ; :: thesis: x in Fr (Ball U,r)
then A12: ( x = <*(u1 - r)*> or x = <*(u1 + r)*> ) by TARSKI:def 2;
A13: ( u1 - r is Real & u1 + r is Real ) by XREAL_0:def 1;
assume A14: not x in Fr (Ball U,r) ; :: thesis: contradiction
u1 + (- r) <= u1 + r by A2, XREAL_1:8;
then x in cl_Ball u,r by A5, A12, A13;
then x in Ball u,r by A4, A14, 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:97; :: thesis: verum