let r, s, a be real number ; :: thesis: ( r <= s implies for p being Point of (Closed-Interval-MSpace r,s) holds
( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ ) )
set M = Closed-Interval-MSpace r,s;
assume r <= s ; :: thesis: for p being Point of (Closed-Interval-MSpace r,s) holds
( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ )
then A1: the carrier of (Closed-Interval-MSpace r,s) = [.r,s.] by TOPMETR:14;
let p be Point of (Closed-Interval-MSpace r,s); :: thesis: ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ )
set B = Ball p,a;
reconsider p1 = p as Point of RealSpace by TOPMETR:12;
set B1 = Ball p1,a;
A2: Ball p,a = (Ball p1,a) /\ the carrier of (Closed-Interval-MSpace r,s) by TOPMETR:13;
( a is Real & p1 is Real ) by XREAL_0:def 1;
then A3: Ball p1,a = ].(p1 - a),(p1 + a).[ by FRECHET:7;

per cases ( ( p1 + a <= s & p1 - a < r ) or ( p1 + a <= s & p1 - a >= r ) or ( p1 + a > s & p1 - a < r ) or ( p1 + a > s & p1 - a >= r ) ) ;

suppose that A4: p1 + a <= s and
A5: p1 - a < r ; :: thesis: ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ )

Ball p,a = [.r,(p1 + a).[

proof

thus Ball p,a c= [.r,(p1 + a).[ :: according to XBOOLE_0:def 10 :: thesis: [.r,(p1 + a).[ c= Ball p,a

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball p,a or b in [.r,(p1 + a).[ )
assume A6: b in Ball p,a ; :: thesis: b in [.r,(p1 + a).[
then reconsider b = b as Element of Ball p,a ;
b in Ball p1,a by A2, A6, XBOOLE_0:def 4;
then A7: b < p1 + a by A3, XXREAL_1:4;
r <= b by A1, A6, XXREAL_1:1;
hence b in [.r,(p1 + a).[ by A7, XXREAL_1:3; :: thesis: verum

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in [.r,(p1 + a).[ or b in Ball p,a )
assume A8: b in [.r,(p1 + a).[ ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
A9: r <= b by A8, XXREAL_1:3;
A10: b < p1 + a by A8, XXREAL_1:3;
then b <= s by A4, XXREAL_0:2;
then A11: b in [.r,s.] by A9, XXREAL_1:1;
p1 - a < b by A5, A9, XXREAL_0:2;
then b in Ball p1,a by A3, A10, XXREAL_1:4;
hence b in Ball p,a by A1, A2, A11, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ ) ; :: thesis: verum

end;

suppose that A12: p1 + a <= s and
A13: p1 - a >= r ; :: thesis: ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ )

Ball p,a = ].(p1 - a),(p1 + a).[

proof

thus Ball p,a c= ].(p1 - a),(p1 + a).[ by A2, A3, XBOOLE_1:17; :: according to XBOOLE_0:def 10 :: thesis: ].(p1 - a),(p1 + a).[ c= Ball p,a
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in ].(p1 - a),(p1 + a).[ or b in Ball p,a )
assume A14: b in ].(p1 - a),(p1 + a).[ ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
b < p1 + a by A14, XXREAL_1:4;
then A15: b <= s by A12, XXREAL_0:2;
p1 - a <= b by A14, XXREAL_1:4;
then r <= b by A13, XXREAL_0:2;
then b in [.r,s.] by A15, XXREAL_1:1;
hence b in Ball p,a by A1, A2, A3, A14, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ ) ; :: thesis: verum

end;

suppose that A16: p1 + a > s and
A17: p1 - a < r ; :: thesis: ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ )

Ball p,a = [.r,s.]

proof

thus Ball p,a c= [.r,s.] by A1; :: according to XBOOLE_0:def 10 :: thesis: [.r,s.] c= Ball p,a
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in [.r,s.] or b in Ball p,a )
assume A18: b in [.r,s.] ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
b <= s by A18, XXREAL_1:1;
then A19: b < p1 + a by A16, XXREAL_0:2;
r <= b by A18, XXREAL_1:1;
then p1 - a < b by A17, XXREAL_0:2;
then b in Ball p1,a by A3, A19, XXREAL_1:4;
hence b in Ball p,a by A1, A2, A18, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ ) ; :: thesis: verum

end;

suppose that A20: p1 + a > s and
A21: p1 - a >= r ; :: thesis: ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ )

Ball p,a = ].(p1 - a),s.]

proof

thus Ball p,a c= ].(p1 - a),s.] :: according to XBOOLE_0:def 10 :: thesis: ].(p1 - a),s.] c= Ball p,a

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Ball p,a or b in ].(p1 - a),s.] )
assume A22: b in Ball p,a ; :: thesis: b in ].(p1 - a),s.]
then reconsider b = b as Element of Ball p,a ;
b in Ball p1,a by A2, A22, XBOOLE_0:def 4;
then A23: p1 - a < b by A3, XXREAL_1:4;
b <= s by A1, A22, XXREAL_1:1;
hence b in ].(p1 - a),s.] by A23, XXREAL_1:2; :: thesis: verum

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in ].(p1 - a),s.] or b in Ball p,a )
assume A24: b in ].(p1 - a),s.] ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
A25: b <= s by A24, XXREAL_1:2;
A26: p1 - a < b by A24, XXREAL_1:2;
then r <= b by A21, XXREAL_0:2;
then A27: b in [.r,s.] by A25, XXREAL_1:1;
b < p1 + a by A20, A25, XXREAL_0:2;
then b in Ball p1,a by A3, A26, XXREAL_1:4;
hence b in Ball p,a by A1, A2, A27, XBOOLE_0:def 4; :: thesis: verum

end;

hence ( Ball p,a = [.r,s.] or Ball p,a = [.r,(p + a).[ or Ball p,a = ].(p - a),s.] or Ball p,a = ].(p - a),(p + a).[ ) ; :: thesis: verum

end;

end;