let p be Point of (TOP-REAL 2); for e being Point of (Euclid 2)
for r being Real 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); for r being Real 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; ( 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
; Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
let a be object ; TARSKI:def 3 ( 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)
; 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:8;
reconsider g = q as FinSequence ;
A3:
for x being object 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
object ;
( 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 A4:
x in dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
;
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 A4, TARSKI:def 2;
suppose A5:
x = 1
;
g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . xA6:
((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . 1
= ].((p `1) - r),((p `1) + r).[
by FUNCT_4:63;
A7:
q `1 < (p `1) + r
by A1, A2, Th37;
(p `1) - r < q `1
by A1, A2, Th37;
hence
g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x
by A5, A6, A7, XXREAL_1:4;
verum end; suppose A8:
x = 2
;
g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . xA9:
((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . 2
= ].((p `2) - r),((p `2) + r).[
by FUNCT_4:63;
A10:
q `2 < (p `2) + r
by A1, A2, Th38;
(p `2) - r < q `2
by A1, A2, Th38;
hence
g . x in ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) . x
by A8, A9, A10, XXREAL_1:4;
verum end;
end;
q is Function of (Seg 2),REAL
by EUCLID:23;
then A11:
dom g = {1,2}
by FINSEQ_1:2, FUNCT_2:def 1;
dom ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[)) = {1,2}
by FUNCT_4:62;
hence
a in product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
by A11, A3, CARD_3:9; verum