let p be Point of (TOP-REAL 2); :: thesis: not west_halfline p is Bounded
set Wp = west_halfline p;
set p11 = p `1 ;
set p12 = p `2 ;
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 and
A2: 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;
set EX1 = (p `1 ) - (2 * r);
reconsider p1 = p, EX = |[((p `1 ) - (2 * r)),(p `2 )]| as Point of (Euclid 2) by EUCLID:71;
0 + (p `1 ) <= (2 * r) + (p `1 ) by A1, XREAL_1:8;
then (p `1 ) - (2 * r) <= p `1 by XREAL_1:22;
then A3: |[((p `1 ) - (2 * r)),(p `2 )]| `1 <= p `1 by EUCLID:56;
then A4: p1 in west_halfline p by TOPREAL1:def 15;
|[((p `1 ) - (2 * r)),(p `2 )]| `2 = p `2 by EUCLID:56;
then A5: EX in west_halfline p by A3, TOPREAL1:def 15;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then dist p1,EX = sqrt ((((p `1 ) - ((p `1 ) - (2 * r))) ^2 ) + (((p `2 ) - (p `2 )) ^2 )) by GOBOARD6:9
.= 2 * r by A1, SQUARE_1:89 ;
hence contradiction by A1, A2, A5, A4, XREAL_1:157; :: thesis: verum