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