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