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 & p1 `1 <= 1 & - 3 <= p1 `2 & 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 A3: 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
A4: p2 = x and
A5: ( - 1 <= p2 `1 & p2 `1 <= 1 & - 3 <= p2 `2 & p2 `2 <= 3 ) by A3;
A6: 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, A5, TOPREAL6:104;
then dist p1,p2 < 10 by XXREAL_0:2;
then |.(x - p).| < 10 by A1, A4, A6, SPPOL_1:62;
hence x in Ball p,10 by TOPREAL9:7; :: thesis: verum