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))

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

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 {<*(u1 - r)*>,<*(u1 + r)*>} or x in Fr (Ball (U,r)) )
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;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

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