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