let a, r, s be Real; :: 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:10;

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:8;

set B1 = Ball (p1,a);

A2: Ball (p,a) = (Ball (p1,a)) /\ the carrier of (Closed-Interval-MSpace (r,s)) by TOPMETR:9;

A3: Ball (p1,a) = ].(p1 - a),(p1 + a).[ by FRECHET:7;

( 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:10;

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:8;

set B1 = Ball (p1,a);

A2: Ball (p,a) = (Ball (p1,a)) /\ the carrier of (Closed-Interval-MSpace (r,s)) by TOPMETR:9;

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

end;

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

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

end;proof

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
thus
Ball (p,a) c= [.r,(p1 + a).[
:: according to XBOOLE_0:def 10 :: thesis: [.r,(p1 + a).[ c= 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;proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in [.r,(p1 + a).[ or b in Ball (p,a) )
let b be object ; :: 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;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

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

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

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

end;proof

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
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 object ; :: 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;let b be object ; :: 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

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

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.]

end;proof

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
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 object ; :: 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;let b be object ; :: 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

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

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.]

end;proof

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
thus
Ball (p,a) c= ].(p1 - a),s.]
:: according to XBOOLE_0:def 10 :: thesis: ].(p1 - a),s.] c= 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;proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in ].(p1 - a),s.] or b in Ball (p,a) )
let b be object ; :: 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;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

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