let e be Point of (Euclid 2); :: thesis: for D being non empty Subset of (TOP-REAL 2)
for r being real number 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 number st D = Ball e,r holds
not D is horizontal
let r be real number ; :: thesis: ( D = Ball e,r implies not D is horizontal )
reconsider p = e as Point of (TOP-REAL 2) by TOPREAL3:13;
assume A1: D = Ball e,r ; :: thesis: not D is horizontal
then A2: r > 0 by TBSP_1:17;
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:16, TBSP_1:17; :: thesis: ( q in D & not p `2 = q `2 )
reconsider f = q as Point of (Euclid 2) by TOPREAL3:13;
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:12
.= sqrt ((((p `1 ) - (p `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 )) by EUCLID:56
.= sqrt (0 + (((p `2 ) - ((p `2 ) - (r / 2))) ^2 )) by EUCLID:56
.= r / 2 by A2, SQUARE_1:89 ;
then dist e,f < r by A1, TBSP_1:17, XREAL_1:218;
hence q in D by A1, METRIC_1:12; :: thesis: not p `2 = q `2
r / 2 > 0 by A2, XREAL_1:141;
then (p `2 ) - (r / 2) < (p `2 ) - 0 by XREAL_1:17;
hence not p `2 = q `2 by EUCLID:56; :: thesis: verum