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