let e be Point of (Euclid 2); for D being non empty Subset of (TOP-REAL 2)
for r being Real st D = Ball (e,r) holds
not D is horizontal
let D be non empty Subset of (TOP-REAL 2); for r being Real st D = Ball (e,r) holds
not D is horizontal
let r be Real; ( D = Ball (e,r) implies not D is horizontal )
reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:8;
assume A1:
D = Ball (e,r)
; not D is horizontal
then A2:
r > 0
by TBSP_1:12;
take
p
; SPPOL_1:def 2 ex b1 being Element of the carrier of (TOP-REAL 2) st
( p in D & b1 in D & not p `2 = b1 `2 )
take q = |[(p `1),((p `2) - (r / 2))]|; ( p in D & q in D & not p `2 = q `2 )
thus
p in D
by A1, TBSP_1:11, TBSP_1:12; ( q in D & not p `2 = q `2 )
reconsider f = q as Point of (Euclid 2) by TOPREAL3:8;
dist (e,f) =
(Pitag_dist 2) . (e,f)
by METRIC_1:def 1
.=
sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2))
by TOPREAL3:7
.=
sqrt ((((p `1) - (p `1)) ^2) + (((p `2) - (q `2)) ^2))
by EUCLID:52
.=
sqrt (0 + (((p `2) - ((p `2) - (r / 2))) ^2))
by EUCLID:52
.=
r / 2
by A2, SQUARE_1:22
;
then
dist (e,f) < r
by A1, TBSP_1:12, XREAL_1:216;
hence
q in D
by A1, METRIC_1:11; not p `2 = q `2
r / 2 > 0
by A2, XREAL_1:139;
then
(p `2) - (r / 2) < (p `2) - 0
by XREAL_1:15;
hence
not p `2 = q `2
by EUCLID:52; verum