let p, p1, q be Point of (TOP-REAL 2); :: thesis:
let r be Real; :: thesis:
let u be Point of (Euclid 2); :: thesis:
set v = |[(p `1),(q `2)]|;
assume that
A1: not p1 in Ball (u,r) and
A2: p in Ball (u,r) and
A3: |[(p `1),(q `2)]| in Ball (u,r) and
A4: not |[(p `1),(q `2)]| in LSeg (p1,p) and
A5: p1 `1 = p `1 and
A6: p `1 <> q `1 and
A7: p `2 <> q `2 ; :: thesis:
A8: LSeg (p,|[(p `1),(q `2)]|) c= Ball (u,r) by A2, A3, Th21;
p in LSeg (p,|[(p `1),(q `2)]|) by RLTOPSP1:68;
then ( p in LSeg (p1,p) & p in (LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q)) ) by RLTOPSP1:68, XBOOLE_0:def 3;
then p in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) by XBOOLE_0:def 4;
then A9: {p} c= ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) by ZFMISC_1:31;
A10: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = ((LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p))) \/ ((LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p))) by XBOOLE_1:23;
A11: p1 = |[(p `1),(p1 `2)]| by A5, EUCLID:53;
A12: q = |[(q `1),(q `2)]| by EUCLID:53;
A13: p = |[(p `1),(p `2)]| by EUCLID:53;
A14: |[(p `1),(q `2)]| `1 = p `1 by EUCLID:52;
A15: |[(p `1),(q `2)]| `2 = q `2 by EUCLID:52;

per cases ;

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

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A1, A2, A5, Th6; :: thesis:

end;

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

now :: thesis:

per cases by A16, XXREAL_0:1;

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

now :: thesis:

per cases by A6, XXREAL_0:1;

suppose A18: p `1 > q `1 ; :: thesis:

now :: thesis:

per cases by A7, XXREAL_0:1;

case A19: p `2 > q `2 ; :: thesis:

then A20: p `2 >= |[(p `1),(q `2)]| `2 by EUCLID:52;
((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A21: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis:

now :: thesis:

per cases by A10, A21, XBOOLE_0:def 3;

case A22: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; :: thesis:

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q1 `2 & q1 `2 <= p1 `2 ) } by A17, A20;
then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A17, A19, Th9, XXREAL_0:2;
hence x in {p} by A22, TOPREAL1:8; :: thesis:

end;

case A23: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; :: thesis:

then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) } by A12, A18, Th10;
then A24: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) ;
x in LSeg (p1,p) by A23, XBOOLE_0:def 4;
then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) } by A11, A13, A17, Th9;
then ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) ;
hence contradiction by A19, A24; :: thesis:

end;

end;

end;

hence x in {p} ; :: thesis:

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9; :: thesis:

end;

case A25: p `2 < q `2 ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose A26: q `2 > p1 `2 ; :: thesis:

then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= |[(p `1),(q `2)]| `2 ) } by A5, A15, A17;
then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A17, A26, Th9, XXREAL_0:2;
hence contradiction by A1, A8; :: thesis:

end;

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

hence contradiction by A1, A3, A5, EUCLID:53; :: thesis:

end;

suppose A27: q `2 < p1 `2 ; :: thesis:

then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= p1 `2 ) } by A14, A15, A25;
hence contradiction by A4, A11, A13, A25, A27, Th9, XXREAL_0:2; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

suppose A28: p `1 < q `1 ; :: thesis:

now :: thesis:

per cases by A7, XXREAL_0:1;

case A29: p `2 > q `2 ; :: thesis:

then A30: p `2 >= |[(p `1),(q `2)]| `2 by EUCLID:52;
((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A31: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis:

now :: thesis:

per cases by A10, A31, XBOOLE_0:def 3;

case A32: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; :: thesis:

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q1 `2 & q1 `2 <= p1 `2 ) } by A17, A30;
then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A17, A29, Th9, XXREAL_0:2;
hence x in {p} by A32, TOPREAL1:8; :: thesis:

end;

case A33: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; :: thesis:

then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A12, A28, Th10;
then A34: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) ;
x in LSeg (p1,p) by A33, XBOOLE_0:def 4;
then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) } by A11, A13, A17, Th9;
then ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) ;
hence contradiction by A29, A34; :: thesis:

end;

end;

end;

hence x in {p} ; :: thesis:

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9; :: thesis:

end;

case A35: p `2 < q `2 ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose A36: q `2 > p1 `2 ; :: thesis:

then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= |[(p `1),(q `2)]| `2 ) } by A5, A15, A17;
then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A17, A36, Th9, XXREAL_0:2;
hence contradiction by A1, A8; :: thesis:

end;

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

hence contradiction by A1, A3, A5, EUCLID:53; :: thesis:

end;

suppose A37: q `2 < p1 `2 ; :: thesis:

then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= p1 `2 ) } by A14, A15, A35;
hence contradiction by A4, A11, A13, A35, A37, Th9, XXREAL_0:2; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

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

now :: thesis:

per cases by A6, XXREAL_0:1;

suppose A39: p `1 > q `1 ; :: thesis:

now :: thesis:

per cases by A7, XXREAL_0:1;

case A40: p `2 > q `2 ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose A41: q `2 > p1 `2 ; :: thesis:

then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p1 `2 <= p2 `2 & p2 `2 <= p `2 ) } by A14, A15, A40;
hence contradiction by A4, A11, A13, A40, A41, Th9, XXREAL_0:2; :: thesis:

end;

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

hence contradiction by A1, A3, A5, EUCLID:53; :: thesis:

end;

suppose A42: q `2 < p1 `2 ; :: thesis:

then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q2 `2 & q2 `2 <= p `2 ) } by A5, A15, A38;
then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A38, A42, Th9, XXREAL_0:2;
hence contradiction by A1, A8; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

case A43: p `2 < q `2 ; :: thesis:

((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A44: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis:

now :: thesis:

per cases by A10, A44, XBOOLE_0:def 3;

case A45: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; :: thesis:

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & p1 `2 <= q1 `2 & q1 `2 <= |[(p `1),(q `2)]| `2 ) } by A15, A38, A43;
then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A38, A43, Th9, XXREAL_0:2;
hence x in {p} by A45, TOPREAL1:8; :: thesis:

end;

case A46: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; :: thesis:

then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) } by A12, A39, Th10;
then A47: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) ;
x in LSeg (p1,p) by A46, XBOOLE_0:def 4;
then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) } by A11, A13, A38, Th9;
then ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) ;
hence contradiction by A43, A47; :: thesis:

end;

end;

end;

hence x in {p} ; :: thesis:

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

suppose A48: p `1 < q `1 ; :: thesis:

now :: thesis:

per cases by A7, XXREAL_0:1;

case A49: p `2 > q `2 ; :: thesis:

now :: thesis:

per cases by XXREAL_0:1;

suppose A50: q `2 > p1 `2 ; :: thesis:

then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p1 `2 <= p2 `2 & p2 `2 <= p `2 ) } by A14, A15, A49;
hence contradiction by A4, A11, A13, A49, A50, Th9, XXREAL_0:2; :: thesis:

end;

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

hence contradiction by A1, A3, A5, EUCLID:53; :: thesis:

end;

suppose A51: q `2 < p1 `2 ; :: thesis:

then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q2 `2 & q2 `2 <= p `2 ) } by A5, A15, A38;
then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A38, A51, Th9, XXREAL_0:2;
hence contradiction by A1, A8; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

case A52: p `2 < q `2 ; :: thesis:

((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A53: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis:

now :: thesis:

per cases by A10, A53, XBOOLE_0:def 3;

case A54: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; :: thesis:

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & p1 `2 <= q1 `2 & q1 `2 <= |[(p `1),(q `2)]| `2 ) } by A15, A38, A52;
then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A38, A52, Th9, XXREAL_0:2;
hence x in {p} by A54, TOPREAL1:8; :: thesis:

end;

case A55: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; :: thesis:

then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A12, A48, Th10;
then A56: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) ;
x in LSeg (p1,p) by A55, XBOOLE_0:def 4;
then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) } by A11, A13, A38, Th9;
then ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) ;
hence contradiction by A52, A56; :: thesis:

end;

end;

end;

hence x in {p} ; :: thesis:

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

end;

end;

hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; :: thesis:

end;

end;