let p be Point of (TOP-REAL 2); :: thesis: ( p in closed_inside_of_rectangle ((- 1),1,(- 3),3) implies closed_inside_of_rectangle ((- 1),1,(- 3),3) c= Ball (p,10) )
assume p in closed_inside_of_rectangle ((- 1),1,(- 3),3) ; :: thesis: closed_inside_of_rectangle ((- 1),1,(- 3),3) c= Ball (p,10)
then consider p1 being Point of (TOP-REAL 2) such that
A1: p1 = p and
A2: - 1 <= p1 `1 and
A3: p1 `1 <= 1 and
A4: - 3 <= p1 `2 and
A5: p1 `2 <= 3 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in closed_inside_of_rectangle ((- 1),1,(- 3),3) or x in Ball (p,10) )
assume A6: x in closed_inside_of_rectangle ((- 1),1,(- 3),3) ; :: thesis: x in Ball (p,10)
then reconsider x = x as Point of (TOP-REAL 2) ;
consider p2 being Point of (TOP-REAL 2) such that
A7: p2 = x and
A8: - 1 <= p2 `1 and
A9: p2 `1 <= 1 and
A10: - 3 <= p2 `2 and
A11: p2 `2 <= 3 by A6;
A12: ex s, t being Point of (Euclid 2) st
( s = p1 & t = p2 & dist (p1,p2) = dist (s,t) ) by TOPREAL6:def 1;
dist (p1,p2) <= (1 - (- 1)) + (3 - (- 3)) by A2, A3, A4, A5, A8, A9, A10, A11, TOPREAL6:95;
then dist (p1,p2) < 10 by XXREAL_0:2;
then |.(x - p).| < 10 by A1, A7, A12, SPPOL_1:39;
hence x in Ball (p,10) by TOPREAL9:7; :: thesis: verum