let e be Point of (Euclid 2); :: thesis: 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); :: thesis: for r being Real st D = Ball (e,r) holds
not D is horizontal
let r be Real; :: thesis: ( 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) ; :: thesis: not D is horizontal
then A2: r > 0 by TBSP_1:12;
take p ; :: according to SPPOL_1:def 2 :: thesis: ex b₁ being Element of the carrier of (TOP-REAL 2) st
( p in D & b₁ in D & not p `2 = b<sub>1</sub> `2 )
take q = |[(p `1),((p `2) - (r / 2))]|; :: thesis: ( p in D & q in D & not p `2 = q `2 )
thus p in D by A1, TBSP_1:11, TBSP_1:12; :: thesis: ( 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))
.= sqrt (0 + (((p `2) - ((p `2) - (r / 2))) ^2))
.= 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; :: thesis: 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 ; :: thesis: verum