let p be Point of (TOP-REAL 2); 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
; contradiction
then reconsider C = north_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 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:67;
A3:
|[(p `1),((p `2) + (2 * r))]| `1 = p `1
by EUCLID:52;
then A4:
p1 in north_halfline p
by TOPREAL1:def 10;
0 + (p `2) <= (2 * r) + (p `2)
by A1, XREAL_1:6;
then
|[(p `1),((p `2) + (2 * r))]| `2 >= p `2
by EUCLID:52;
then A5:
EX in north_halfline p
by A3, TOPREAL1:def 10;
p = |[(p `1),(p `2)]|
by EUCLID:53;
then dist (p1,EX) =
sqrt ((((p `1) - (p `1)) ^2) + (((p `2) - ((p `2) + (2 * r))) ^2))
by GOBOARD6:6
.=
sqrt (((((p `2) + (2 * r)) - (p `2)) ^2) + 0)
.=
2 * r
by A1, SQUARE_1:22
;
hence
contradiction
by A1, A2, A5, A4, XREAL_1:155; verum