let r, s, a be real number ; :: thesis: ( r <= s & 0 < a 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 that
A1: r <= s and
A2: 0 < a ; :: 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).[ )
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;
A3: the carrier of (Closed-Interval-MSpace r,s) = [.r,s.] by A1, TOPMETR:14;
reconsider p1 = p as Point of RealSpace by TOPMETR:12;
set B1 = Ball p1,a;
A4: 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 A5: Ball p1,a = ].(p1 - a),(p1 + a).[ by A2, 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 A6: p1 + a <= s and
A7: 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 A8: 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 A4, A8, XBOOLE_0:def 4;
then A9: b < p1 + a by A5, XXREAL_1:4;
r <= b by A3, A8, XXREAL_1:1;
hence b in [.r,(p1 + a).[ by A9, 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 A10: b in [.r,(p1 + a).[ ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
A11: r <= b by A10, XXREAL_1:3;
A12: b < p1 + a by A10, XXREAL_1:3;
then b <= s by A6, XXREAL_0:2;
then A13: b in [.r,s.] by A11, XXREAL_1:1;
p1 - a < b by A7, A11, XXREAL_0:2;
then b in Ball p1,a by A5, A12, XXREAL_1:4;
hence b in Ball p,a by A3, A4, A13, 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 A14: p1 + a <= s and
A15: 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 A4, A5, 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 A16: b in ].(p1 - a),(p1 + a).[ ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
p1 - a <= b by A16, XXREAL_1:4;
then A17: r <= b by A15, XXREAL_0:2;
b < p1 + a by A16, XXREAL_1:4;
then b <= s by A14, XXREAL_0:2;
then b in [.r,s.] by A17, XXREAL_1:1;
hence b in Ball p,a by A3, A4, A5, A16, 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 A18: p1 + a > s and
A19: 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 A3; :: 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 A20: b in [.r,s.] ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
A21: r <= b by A20, XXREAL_1:1;
b <= s by A20, XXREAL_1:1;
then A22: b < p1 + a by A18, XXREAL_0:2;
p1 - a < b by A19, A21, XXREAL_0:2;
then b in Ball p1,a by A5, A22, XXREAL_1:4;
hence b in Ball p,a by A3, A4, A20, 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 A23: p1 + a > s and
A24: 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 A25: 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 A4, A25, XBOOLE_0:def 4;
then A26: p1 - a < b by A5, XXREAL_1:4;
b <= s by A3, A25, XXREAL_1:1;
hence b in ].(p1 - a),s.] by A26, 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 A27: b in ].(p1 - a),s.] ; :: thesis: b in Ball p,a
then reconsider b = b as Real ;
A28: b <= s by A27, XXREAL_1:2;
A29: p1 - a < b by A27, XXREAL_1:2;
then r <= b by A24, XXREAL_0:2;
then A30: b in [.r,s.] by A28, XXREAL_1:1;
b < p1 + a by A23, A28, XXREAL_0:2;
then b in Ball p1,a by A5, A29, XXREAL_1:4;
hence b in Ball p,a by A3, A4, A30, 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;