let p be Point of (TOP-REAL 2); :: thesis: not west_halfline p is Bounded
set Wp = west_halfline p;
assume west_halfline p is Bounded ; :: thesis: contradiction
then reconsider C = west_halfline p as bounded Subset of (Euclid 2) by Def2;
consider r being Real such that
A1: ( 0 < r & ( for x, y being Point of (Euclid 2) st x in C & y in C holds
dist x,y <= r ) ) by TBSP_1:def 9;
reconsider p1 = p, EX = |[((p `1 ) - (2 * r)),(p `2 )]| as Point of (Euclid 2) by Lm2;
A2: 0 <= 2 * r by A1;
then 0 + (p `1 ) <= (2 * r) + (p `1 ) by XREAL_1:8;
then (p `1 ) - (2 * r) <= p `1 by XREAL_1:22;
then ( |[((p `1 ) - (2 * r)),(p `2 )]| `1 <= p `1 & |[((p `1 ) - (2 * r)),(p `2 )]| `2 = p `2 ) by EUCLID:56;
then A3: ( EX in west_halfline p & p1 in west_halfline p ) by TOPREAL1:def 15;
set EX1 = (p `1 ) - (2 * r);
set p11 = p `1 ;
set p12 = p `2 ;
A4: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A5: r < 2 * r by A1, XREAL_1:157;
dist p1,EX = sqrt ((((p `1 ) - ((p `1 ) - (2 * r))) ^2 ) + (((p `2 ) - (p `2 )) ^2 )) by A4, GOBOARD6:9
.= 2 * r by A2, SQUARE_1:89 ;
hence contradiction by A1, A3, A5; :: thesis: verum