let p be Point of (TOP-REAL 2); for e being Point of (Euclid 2)
for P being Subset of (TOP-REAL 2)
for r being Real st P = Ball (e,r) & p = e holds
proj1 .: P = ].((p `1) - r),((p `1) + r).[
let e be Point of (Euclid 2); for P being Subset of (TOP-REAL 2)
for r being Real st P = Ball (e,r) & p = e holds
proj1 .: P = ].((p `1) - r),((p `1) + r).[
let P be Subset of (TOP-REAL 2); for r being Real st P = Ball (e,r) & p = e holds
proj1 .: P = ].((p `1) - r),((p `1) + r).[
let r be Real; ( P = Ball (e,r) & p = e implies proj1 .: P = ].((p `1) - r),((p `1) + r).[ )
assume that
A1:
P = Ball (e,r)
and
A2:
p = e
; proj1 .: P = ].((p `1) - r),((p `1) + r).[
hereby TARSKI:def 3,
XBOOLE_0:def 10 ].((p `1) - r),((p `1) + r).[ c= proj1 .: P
let a be
object ;
( a in proj1 .: P implies a in ].((p `1) - r),((p `1) + r).[ )assume
a in proj1 .: P
;
a in ].((p `1) - r),((p `1) + r).[then consider x being
object such that A3:
x in the
carrier of
(TOP-REAL 2)
and A4:
x in P
and A5:
a = proj1 . x
by FUNCT_2:64;
reconsider b =
a as
Real by A5;
reconsider x =
x as
Point of
(TOP-REAL 2) by A3;
A6:
a = x `1
by A5, PSCOMP_1:def 5;
then A7:
b < (p `1) + r
by A1, A2, A4, Th37;
(p `1) - r < b
by A1, A2, A4, A6, Th37;
hence
a in ].((p `1) - r),((p `1) + r).[
by A7, XXREAL_1:4;
verum
end;
let a be object ; TARSKI:def 3 ( not a in ].((p `1) - r),((p `1) + r).[ or a in proj1 .: P )
assume A8:
a in ].((p `1) - r),((p `1) + r).[
; a in proj1 .: P
then reconsider b = a as Real ;
reconsider f = |[b,(p `2)]| as Point of (Euclid 2) by TOPREAL3:8;
A9: dist (f,e) =
(Pitag_dist 2) . (f,e)
by METRIC_1:def 1
.=
sqrt ((((|[b,(p `2)]| `1) - (p `1)) ^2) + (((|[b,(p `2)]| `2) - (p `2)) ^2))
by A2, TOPREAL3:7
.=
sqrt (((b - (p `1)) ^2) + (((|[b,(p `2)]| `2) - (p `2)) ^2))
by EUCLID:52
.=
sqrt (((b - (p `1)) ^2) + (((p `2) - (p `2)) ^2))
by EUCLID:52
.=
sqrt (((b - (p `1)) ^2) + 0)
;
b < (p `1) + r
by A8, XXREAL_1:4;
then A10:
b - (p `1) < ((p `1) + r) - (p `1)
by XREAL_1:9;
then A13:
|[b,(p `2)]| in P
by A1, METRIC_1:11;
a =
|[b,(p `2)]| `1
by EUCLID:52
.=
proj1 . |[b,(p `2)]|
by PSCOMP_1:def 5
;
hence
a in proj1 .: P
by A13, FUNCT_2:35; verum