let U be Point of (TOP-REAL 1); :: thesis: for r, u1 being Real st <*u1*> = U & r > 0 holds
Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>}
let r, u1 be Real; :: 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 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)*>} :: according to XBOOLE_0:def 10 :: thesis: {<*(u1 - r)*>,<*(u1 + r)*>} c= Fr (Ball (U,r))
proof
let x be object ; :: 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 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)*>} ; :: 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 object ; :: 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;
assume A13: not x in Fr (Ball (U,r)) ; :: thesis: 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; :: thesis: verum