let p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for r being real number st p = e holds
product (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) c= Ball e,r
let e be Point of (Euclid 2); :: thesis: for r being real number st p = e holds
product (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) c= Ball e,r
let r be real number ; :: thesis: ( p = e implies product (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) c= Ball e,r )
set A = ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[;
set B = ].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[;
set f = 1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[;
assume A1: p = e ; :: thesis: product (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) c= Ball e,r
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in product (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) or a in Ball e,r )
assume a in product (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) ; :: thesis: a in Ball e,r
then consider g being Function such that
A2: a = g and
A3: dom g = dom (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) and
A4: for x being set st x in dom (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) holds
g . x in (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) . x by CARD_3:def 5;
A5: ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[ = { m where m is Real : ( (p `1 ) - (r / (sqrt 2)) < m & m < (p `1 ) + (r / (sqrt 2)) ) } by RCOMP_1:def 2;
A6: ].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[ = { n where n is Real : ( (p `2 ) - (r / (sqrt 2)) < n & n < (p `2 ) + (r / (sqrt 2)) ) } by RCOMP_1:def 2;
A7: dom (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) = {1,2} by FUNCT_4:65;
then A8: ( 1 in dom (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) & 2 in dom (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) ) by TARSKI:def 2;
( (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) . 1 = ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[ & (1,2 --> ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[,].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[) . 2 = ].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[ ) by FUNCT_4:66;
then A9: ( g . 1 in ].((p `1 ) - (r / (sqrt 2))),((p `1 ) + (r / (sqrt 2))).[ & g . 2 in ].((p `2 ) - (r / (sqrt 2))),((p `2 ) + (r / (sqrt 2))).[ ) by A4, A8;
then consider m being Real such that
A10: m = g . 1 and
( (p `1 ) - (r / (sqrt 2)) < m & m < (p `1 ) + (r / (sqrt 2)) ) by A5;
consider n being Real such that
A11: n = g . 2 and
( (p `2 ) - (r / (sqrt 2)) < n & n < (p `2 ) + (r / (sqrt 2)) ) by A6, A9;
(p `1 ) + (r / (sqrt 2)) > (p `1 ) - (r / (sqrt 2)) by A9, XXREAL_1:28;
then (p `1 ) - ((p `1 ) + (r / (sqrt 2))) < (p `1 ) - ((p `1 ) - (r / (sqrt 2))) by XREAL_1:17;
then (- (r / (sqrt 2))) + (r / (sqrt 2)) < (r / (sqrt 2)) + (r / (sqrt 2)) by XREAL_1:8;
then A12: 0 < (r + r) / (sqrt 2) by XCMPLX_1:63;
A13: 0 < r by A12, SQUARE_1:84;
A14: dom <*(g . 1),(g . 2)*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;

now

let k be set ; :: thesis: ( k in dom g implies g . k = <*(g . 1),(g . 2)*> . k )
assume k in dom g ; :: thesis: g . k = <*(g . 1),(g . 2)*> . k
then ( k = 1 or k = 2 ) by A3, TARSKI:def 2;
hence g . k = <*(g . 1),(g . 2)*> . k by FINSEQ_1:61; :: thesis: verum

end;

then a = |[m,n]| by A2, A3, A7, A10, A11, A14, FUNCT_1:9;
then reconsider c = a as Point of (TOP-REAL 2) ;
reconsider b = c as Point of (Euclid 2) by TOPREAL3:13;
( 0 <= (m - (p `1 )) ^2 & 0 <= (n - (p `2 )) ^2 ) by XREAL_1:65;
then A15: 0 + 0 <= ((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ) ;
( abs (m - (p `1 )) < r / (sqrt 2) & abs (n - (p `2 )) < r / (sqrt 2) ) by A9, A10, A11, RCOMP_1:8;
then ( (abs (m - (p `1 ))) ^2 < (r / (sqrt 2)) ^2 & (abs (n - (p `2 ))) ^2 < (r / (sqrt 2)) ^2 ) by COMPLEX1:132, SQUARE_1:78;
then ( (abs (m - (p `1 ))) ^2 < (r ^2 ) / ((sqrt 2) ^2 ) & (abs (n - (p `2 ))) ^2 < (r ^2 ) / ((sqrt 2) ^2 ) ) by XCMPLX_1:77;
then ( (abs (m - (p `1 ))) ^2 < (r ^2 ) / 2 & (abs (n - (p `2 ))) ^2 < (r ^2 ) / 2 ) by SQUARE_1:def 4;
then ( (m - (p `1 )) ^2 < (r ^2 ) / 2 & (n - (p `2 )) ^2 < (r ^2 ) / 2 ) by COMPLEX1:161;
then ((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 ) < ((r ^2 ) / 2) + ((r ^2 ) / 2) by XREAL_1:10;
then sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 )) < sqrt (r ^2 ) by A15, SQUARE_1:95;
then A16: sqrt (((m - (p `1 )) ^2 ) + ((n - (p `2 )) ^2 )) < r by A13, SQUARE_1:89;
dist b,e = (Pitag_dist 2) . b,e by METRIC_1:def 1
.= sqrt ((((c `1 ) - (p `1 )) ^2 ) + (((c `2 ) - (p `2 )) ^2 )) by A1, TOPREAL3:12 ;
hence a in Ball e,r by A2, A10, A11, A16, METRIC_1:12; :: thesis: verum