let p, p1, q be Point of (TOP-REAL 2); :: thesis:
let r be Real; :: thesis:
let u be Point of (Euclid 2); :: thesis:
assume that
A1: not p1 in Ball (u,r) and
A2: q in Ball (u,r) and
A3: p in Ball (u,r) and
A4: not p in LSeg (p1,q) ; :: thesis:
assume A5: ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) ; :: thesis:
assume A6: ( p1 `1 = q `1 or p1 `2 = q `2 ) ; :: thesis:

per cases by A6;

suppose p1 `1 = q `1 ; :: thesis:

hence ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A1, A2, Th6; :: thesis:

end;

suppose p1 `2 = q `2 ; :: thesis:

hence ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A1, A2, Th6; :: thesis:

end;

A8: p = |[(p `1),(p `2)]| by EUCLID:53;
A9: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;
A10: q = |[(q `1),(q `2)]| by EUCLID:53;
A11: LSeg (p,q) c= Ball (u,r) by A2, A3, Th21;

now :: thesis:

per cases by A5;

suppose A12: ( q `1 = p `1 & q `2 <> p `2 ) ; :: thesis:

set r = p `1 ;
set pq = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= q `2 ) } ;
set qp = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = p `1 & q `2 <= p3 `2 & p3 `2 <= p `2 ) } ;
set pp1 = { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = p `1 & p `2 <= p11 `2 & p11 `2 <= p1 `2 ) } ;
set p1p = { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = p `1 & p1 `2 <= p22 `2 & p22 `2 <= p `2 ) } ;
set qp1 = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & q `2 <= q1 `2 & q1 `2 <= p1 `2 ) } ;
set p1q = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= q `2 ) } ;

now :: thesis:

per cases by A12, XXREAL_0:1;

suppose A13: q `2 > p `2 ; :: thesis:

now :: thesis:

per cases by A7;

suppose A14: ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; :: thesis:

now :: thesis:

per cases by A14, XXREAL_0:1;

case A15: p1 `2 > q `2 ; :: thesis:

then q in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = p `1 & p `2 <= p11 `2 & p11 `2 <= p1 `2 ) } by A12, A13;
then q in LSeg (p,p1) by A8, A9, A12, A13, A14, A15, Th9, XXREAL_0:2;
hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by TOPREAL1:8; :: thesis:

end;

case A16: p1 `2 < q `2 ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose A17: p1 `2 > p `2 ; :: thesis:

then p1 in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A16;
then p1 in LSeg (p,q) by A8, A10, A12, A16, A17, Th9, XXREAL_0:2;
hence contradiction by A1, A11; :: thesis:

end;

suppose p1 `2 = p `2 ; :: thesis:

hence contradiction by A1, A3, A12, A14, Th6; :: thesis:

end;

suppose p1 `2 < p `2 ; :: thesis:

then p in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= q `2 ) } by A13;
hence contradiction by A4, A9, A10, A12, A14, A16, Th9; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; :: thesis:

end;

suppose ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; :: thesis:

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by A10, A12, Th30; :: thesis:

end;

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; :: thesis:

end;

suppose A18: q `2 < p `2 ; :: thesis:

now :: thesis:

per cases by A7;

suppose A19: ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; :: thesis:

now :: thesis:

per cases by A19, XXREAL_0:1;

case A20: p1 `2 > q `2 ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose p1 `2 > p `2 ; :: thesis:

then p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & q `2 <= q1 `2 & q1 `2 <= p1 `2 ) } by A18;
hence contradiction by A4, A9, A10, A12, A19, A20, Th9; :: thesis:

end;

suppose p1 `2 = p `2 ; :: thesis:

hence contradiction by A1, A3, A12, A19, Th6; :: thesis:

end;

suppose p1 `2 < p `2 ; :: thesis:

then p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = p `1 & q `2 <= p3 `2 & p3 `2 <= p `2 ) } by A12, A19, A20;
then p1 in LSeg (p,q) by A8, A10, A12, A18, Th9;
hence contradiction by A1, A11; :: thesis:

end;

hence contradiction ; :: thesis:

end;

case A21: p1 `2 < q `2 ; :: thesis:

then q in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = p `1 & p1 `2 <= p22 `2 & p22 `2 <= p `2 ) } by A12, A18;
then q in LSeg (p1,p) by A8, A9, A12, A18, A19, A21, Th9, XXREAL_0:2;
hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by TOPREAL1:8; :: thesis:

end;

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; :: thesis:

end;

suppose ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; :: thesis:

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by A10, A12, Th30; :: thesis:

end;

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; :: thesis:

end;

hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; :: thesis:

end;

suppose A22: ( q `1 <> p `1 & q `2 = p `2 ) ; :: thesis:

set r = p `2 ;
set pq = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } ;
set qp = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = p `2 & q `1 <= p3 `1 & p3 `1 <= p `1 ) } ;
set pp1 = { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & p `1 <= p11 `1 & p11 `1 <= p1 `1 ) } ;
set p1p = { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = p `2 & p1 `1 <= p22 `1 & p22 `1 <= p `1 ) } ;
set qp1 = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & q `1 <= q1 `1 & q1 `1 <= p1 `1 ) } ;
set p1q = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= q `1 ) } ;