let a, r, s be Real; :: thesis: ( r <= s implies for p being Point of () 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 () 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 () = [.r,s.] by TOPMETR:10;
let p be Point of (); :: 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 () 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 ) ) ;
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 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 ;
then A7: b < p1 + a by ;
r <= b by ;
hence b in [.r,(p1 + a).[ by ; :: thesis: verum
end;
let b be object ; :: 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 ;
A10: b < p1 + a by ;
then b <= s by ;
then A11: b in [.r,s.] by ;
p1 - a < b by ;
then b in Ball (p1,a) by ;
hence b in Ball (p,a) by ; :: 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 ; :: 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 ;
then A15: b <= s by ;
p1 - a <= b by ;
then r <= b by ;
then b in [.r,s.] by ;
hence b in Ball (p,a) by ; :: 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 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 ;
then A19: b < p1 + a by ;
r <= b by ;
then p1 - a < b by ;
then b in Ball (p1,a) by ;
hence b in Ball (p,a) by ; :: 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 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 ;
then A23: p1 - a < b by ;
b <= s by ;
hence b in ].(p1 - a),s.] by ; :: thesis: verum
end;
let b be object ; :: 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 ;
A26: p1 - a < b by ;
then r <= b by ;
then A27: b in [.r,s.] by ;
b < p1 + a by ;
then b in Ball (p1,a) by ;
hence b in Ball (p,a) by ; :: 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;