let p be Point of (TOP-REAL 2); :: thesis: not east_halfline p is bounded
set Wp = east_halfline p;
set p11 = p `1 ;
set p12 = p `2 ;
assume east_halfline p is bounded ; :: thesis: contradiction
then reconsider C = east_halfline p as bounded Subset of (Euclid 2) by Th5;
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 7;
set EX1 = (p `1) + (2 * r);
set EX2 = p `2 ;
reconsider p1 = p, EX = |[((p `1) + (2 * r)),(p `2)]| as Point of (Euclid 2) by EUCLID:67;
0 + (p `1) <= (2 * r) + (p `1) by A1, XREAL_1:6;
then A3: |[((p `1) + (2 * r)),(p `2)]| `1 >= p `1 ;
then A4: p1 in east_halfline p by TOPREAL1:def 11;
|[((p `1) + (2 * r)),(p `2)]| `2 = p `2 ;
then A5: EX in east_halfline p by A3, TOPREAL1:def 11;
p = |[(p `1),(p `2)]| by EUCLID:53;
then dist (p1,EX) = sqrt ((((p `1) - ((p `1) + (2 * r))) ^2) + (((p `2) - (p `2)) ^2)) by GOBOARD6:6
.= sqrt (((((p `1) + (2 * r)) - (p `1)) ^2) + 0)
.= 2 * r by A1, SQUARE_1:22 ;
hence contradiction by A1, A2, A5, A4, XREAL_1:155; :: thesis: verum