let p be Point of (TOP-REAL 2); :: thesis: not east_halfline p is Bounded
set Wp = east_halfline p;
assume east_halfline p is Bounded ; :: thesis: contradiction
then reconsider C = east_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;
set EX1 = (p `1 ) + (2 * r);
set EX2 = p `2 ;
set p11 = p `1 ;
set p12 = p `2 ;
A2: 0 <= 2 * r by A1;
then 0 + (p `1 ) <= (2 * r) + (p `1 ) by XREAL_1:8;
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 east_halfline p & p1 in east_halfline p ) by TOPREAL1:def 13;
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
.= sqrt (((((p `1 ) + (2 * r)) - (p `1 )) ^2 ) + 0 )
.= 2 * r by A2, SQUARE_1:89 ;
hence contradiction by A1, A3, A5; :: thesis: verum