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
Ball e,r c= product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[)
let e be Point of (Euclid 2); :: thesis: for r being real number st p = e holds
Ball e,r c= product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[)
let r be real number ; :: thesis: ( p = e implies Ball e,r c= product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) )
set A = ].((p `1 ) - r),((p `1 ) + r).[;
set B = ].((p `2 ) - r),((p `2 ) + r).[;
set f = 1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[;
assume A1: p = e ; :: thesis: Ball e,r c= product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Ball e,r or a in product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) )
assume A2: a in Ball e,r ; :: thesis: a in product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[)
then reconsider b = a as Point of (Euclid 2) ;
reconsider q = b as Point of (TOP-REAL 2) by TOPREAL3:13;
reconsider g = q as FinSequence ;
A3: dom (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) = {1,2} by FUNCT_4:65;
q is Function of (Seg 2),REAL by EUCLID:26;
then A4: dom g = {1,2} by FINSEQ_1:4, FUNCT_2:def 1;
for x being set st x in dom (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) holds
g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x

proof

let x be set ; :: thesis: ( x in dom (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) implies g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x )
assume A5: x in dom (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) ; :: thesis: g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x

per cases ( x = 1 or x = 2 ) by A5, TARSKI:def 2;

suppose A6: x = 1 ; :: thesis: g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x

A7: (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . 1 = ].((p `1 ) - r),((p `1 ) + r).[ by FUNCT_4:66;
( (p `1 ) - r < q `1 & q `1 < (p `1 ) + r ) by A1, A2, Th47;
hence g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x by A6, A7, XXREAL_1:4; :: thesis: verum

end;

suppose A8: x = 2 ; :: thesis: g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x

A9: (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . 2 = ].((p `2 ) - r),((p `2 ) + r).[ by FUNCT_4:66;
( (p `2 ) - r < q `2 & q `2 < (p `2 ) + r ) by A1, A2, Th48;
hence g . x in (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) . x by A8, A9, XXREAL_1:4; :: thesis: verum

end;

end;

end;

hence a in product (1,2 --> ].((p `1 ) - r),((p `1 ) + r).[,].((p `2 ) - r),((p `2 ) + r).[) by A3, A4, CARD_3:18; :: thesis: verum