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 set ; :: 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:104;
then dist p1,p2 < 10 by XXREAL_0:2;
then |.(x - p).| < 10 by A1, A7, A12, SPPOL_1:62;
hence x in Ball p,10 by TOPREAL9:7; :: thesis: verum