p`2; then p1 in pq 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; end; suppose p1`2=p`2; hence contradiction by A1,A3,A12,A14,Th6; end; suppose p1`2q`1 & p1`2=q`2; hence thesis by A10,A12,Th30; end; end; hence thesis; end; suppose A18: q`2

q`2; now per cases by A19,XXREAL_0:1; case A20: p1`2>q`2; now per cases by XXREAL_0:1; suppose p1`2>p`2; then p in qp1 by A18; hence contradiction by A4,A9,A10,A12,A19,A20,Th9; end; suppose p1`2=p`2; hence contradiction by A1,A3,A12,A19,Th6; end; suppose p1`2

q`1 & p1`2=q`2; hence thesis by A10,A12,Th30; end; end; hence thesis; end; end; hence thesis; end; suppose A22: q`1<>p`1 & q`2=p`2; set r = p`2, pq = {p2: p2`2=r & p`1<=p2`1 & p2`1<=q`1}, qp = {p3: p3`2=r & q`1<=p3`1 & p3`1<=p`1}, pp1 = {p11: p11`2=r & p`1<=p11`1 & p11`1<=p1`1}, p1p = {p22: p22`2=r & p1`1<=p22`1 & p22`1<=p`1}, qp1 = {q1: q1`2=r & q`1<=q1`1 & q1 `1<=p1`1}, p1q = {q2: q2`2=r & p1`1<=q2`1 & q2`1<=q`1}; now per cases by A22,XXREAL_0:1; suppose A23: q`1>p`1; now per cases by A7; suppose p1`1=q`1 & p1`2<>q`2; hence thesis by A10,A22,Th29; end; suppose A24: p1`1<>q`1 & p1`2=q`2; now per cases by A24,XXREAL_0:1; case A25: p1`1>q`1; then q in pp1 by A22,A23; then q in LSeg(p,p1) by A8,A9,A22,A23,A24,A25,Th10,XXREAL_0:2 ; hence thesis by TOPREAL1:8; end; case A26: p1`1

p`1; then p1 in pq by A22,A24,A26; then p1 in LSeg(p,q) by A8,A10,A22,A26,A27,Th10, XXREAL_0:2; hence contradiction by A1,A11; end; suppose p1`1=p`1; hence contradiction by A1,A3,A22,A24,Th6; end; suppose p1`1q`2; hence thesis by A10,A22,Th29; end; suppose A29: p1`1<>q`1 & p1`2=q`2; now per cases by A29,XXREAL_0:1; case A30: p1`1>q`1; now per cases by XXREAL_0:1; suppose p1`1>p`1; then p in qp1 by A28; hence contradiction by A4,A9,A10,A22,A29,A30,Th10; end; suppose p1`1=p`1; hence contradiction by A1,A3,A22,A29,Th6; end; suppose p1`1

q`1 & p`2<>q`2 implies (LSeg(p,|[ p`1,q`2]|) \/ LSeg(|[p`1,q`2]|,q)) /\ LSeg(p1,p) = {p} proof set v = |[p`1,q`2]|; assume that A1: not p1 in Ball(u,r) and A2: p in Ball(u,r) and A3: v in Ball(u,r) and A4: not v in LSeg(p1,p) and A5: p1`1=p`1 and A6: p`1<>q`1 and A7: p`2<>q`2; A8: LSeg(p,v) c= Ball(u,r) by A2,A3,Th21; p in LSeg(p,v) by RLTOPSP1:68; then p in LSeg(p1,p) & p in LSeg(p,v) \/ LSeg(v,q) by RLTOPSP1:68 ,XBOOLE_0:def 3; then p in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by XBOOLE_0:def 4; then A9: {p} c= (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by ZFMISC_1:31; A10: (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) = LSeg(p,v) /\ LSeg(p1,p) \/ LSeg(v,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: v`1=p`1 by EUCLID:52; A15: v`2=q`2 by EUCLID:52; per cases; suppose p1`2=p`2; hence thesis by A1,A2,A5,Th6; end; suppose A16: p1`2<>p`2; now per cases by A16,XXREAL_0:1; suppose A17: p1`2>p`2; now per cases by A6,XXREAL_0:1; suppose A18: p`1>q`1; now per cases by A7,XXREAL_0:1; case A19: p`2>q`2; then A20: p`2>=v`2 by EUCLID:52; (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p} proof let x be object such that A21: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p); now per cases by A10,A21,XBOOLE_0:def 3; case A22: x in LSeg(p,v) /\ LSeg(p1,p); p in {q1: q1`1=p`1 & v`2<=q1`2 & q1`2<=p1`2} by A17,A20; then p in LSeg(p1,v) by A11,A15,A17,A19,Th9,XXREAL_0:2; hence thesis by A22,TOPREAL1:8; end; case A23: x in LSeg(v,q) /\ LSeg(p1,p); then x in LSeg(v,q) by XBOOLE_0:def 4; then x in {p2: p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1} by A12,A18 ,Th10; then A24: ex p2 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: q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2} by A11,A13 ,A17,Th9; then ex q2 st q2=x & q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2; hence contradiction by A19,A24; end; end; hence thesis; end; hence thesis by A9; end; case A25: p`2

p1`2; then p1 in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=v`2} by A5,A15 ,A17; then p1 in LSeg(p,v) by A13,A15,A17,A26,Th9,XXREAL_0:2; hence contradiction by A1,A8; end; suppose q`2=p1`2; hence contradiction by A1,A3,A5,EUCLID:53; end; suppose A27: q`2q`2; then A30: p`2>=v`2 by EUCLID:52; (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p} proof let x be object such that A31: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p); now per cases by A10,A31,XBOOLE_0:def 3; case A32: x in LSeg(p,v) /\ LSeg(p1,p); p in {q1: q1`1=p`1 & v`2<=q1`2 & q1`2<=p1`2} by A17,A30; then p in LSeg(p1,v) by A11,A15,A17,A29,Th9,XXREAL_0:2; hence thesis by A32,TOPREAL1:8; end; case A33: x in LSeg(v,q) /\ LSeg(p1,p); then x in LSeg(v,q) by XBOOLE_0:def 4; then x in {p2: p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1} by A12,A28 ,Th10; then A34: ex p2 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: q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2} by A11,A13 ,A17,Th9; then ex q2 st q2=x & q2`1=p`1 & p`2 <=q2`2 & q2`2<=p1`2; hence contradiction by A29,A34; end; end; hence thesis; end; hence thesis by A9; end; case A35: p`2 p1`2; then p1 in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=v`2} by A5,A15 ,A17; then p1 in LSeg(p,v) by A13,A15,A17,A36,Th9,XXREAL_0:2; hence contradiction by A1,A8; end; suppose q`2=p1`2; hence contradiction by A1,A3,A5,EUCLID:53; end; suppose A37: q`2q`1; now per cases by A7,XXREAL_0:1; case A40: p`2>q`2; now per cases by XXREAL_0:1; suppose A41: q`2>p1`2; then v in {p2: 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; end; suppose q`2=p1`2; hence contradiction by A1,A3,A5,EUCLID:53; end; suppose A42: q`2 q`2; now per cases by XXREAL_0:1; suppose A50: q`2>p1`2; then v in {p2: 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; end; suppose q`2=p1`2; hence contradiction by A1,A3,A5,EUCLID:53; end; suppose A51: q`2 q`1 & p`2<>q`2 implies (LSeg(p,|[ q`1,p`2]|) \/ LSeg(|[q`1,p`2]|,q)) /\ LSeg(p1,p) = {p} proof set v = |[q`1,p`2]|; assume that A1: not p1 in Ball(u,r) and A2: p in Ball(u,r) and A3: v in Ball(u,r) and A4: not v in LSeg(p1,p) and A5: p1`2=p`2 and A6: p`1<>q`1 and A7: p`2<>q`2; A8: LSeg(p,v) c= Ball(u,r) by A2,A3,Th21; A9: p1=|[p1`1,p`2]| by A5,EUCLID:53; p in LSeg(p,v) by RLTOPSP1:68; then p in LSeg(p1,p) & p in LSeg(p,v) \/ LSeg(v,q) by RLTOPSP1:68 ,XBOOLE_0:def 3; then p in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by XBOOLE_0:def 4; then A10: {p} c= (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by ZFMISC_1:31; A11: (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) = LSeg(p,v) /\ LSeg(p1,p) \/ LSeg(v,q) /\ LSeg(p1,p) by XBOOLE_1:23; A12: q=|[q`1,q`2]| by EUCLID:53; A13: p=|[p`1,p`2]| by EUCLID:53; A14: v`2=p`2 by EUCLID:52; A15: v`1=q`1 by EUCLID:52; per cases; suppose p1`1=p`1; hence thesis by A1,A2,A5,Th6; end; suppose A16: p1`1<>p`1; now per cases by A16,XXREAL_0:1; suppose A17: p1`1>p`1; now per cases by A6,XXREAL_0:1; case A18: p`1>q`1; then A19: p`1>=v`1 by EUCLID:52; now per cases by A7,XXREAL_0:1; suppose A20: p`2>q`2; (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p} proof let x be object such that A21: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p); now per cases by A11,A21,XBOOLE_0:def 3; case A22: x in LSeg(p,v) /\ LSeg(p1,p); p in {q1: q1`2=p`2 & v`1<=q1`1 & q1`1<=p1`1} by A17,A19; then p in LSeg(p1,v) by A9,A15,A17,A18,Th10,XXREAL_0:2; hence thesis by A22,TOPREAL1:8; end; case A23: x in LSeg(v,q) /\ LSeg(p1,p); then x in LSeg(q,v) by XBOOLE_0:def 4; then x in {p2: p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2} by A12,A20 ,Th9; then A24: ex p2 st p2=x & p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2; x in LSeg(p, p1) by A23,XBOOLE_0:def 4; then x in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1} by A9,A13 ,A17,Th10; then ex q2 st q2=x & q2`2=p`2 & p`1 <=q2`1 & q2`1<=p1`1; hence contradiction by A18,A24; end; end; hence thesis; end; hence thesis by A10; end; suppose A25: p`2 p1`1; then p1 in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=v`1} by A5,A15,A17 ; then p1 in LSeg(p,v) by A13,A15,A17,A31,Th10,XXREAL_0:2; hence contradiction by A1,A8; end; suppose q`1=p1`1; hence contradiction by A1,A3,A5,EUCLID:53; end; suppose q`1q`1; now per cases by XXREAL_0:1; suppose q`1>p1`1; then v in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A15,A14,A33; hence contradiction by A4,A9,A13,A32,Th10; end; suppose q`1=p1`1; hence contradiction by A1,A3,A5,EUCLID:53; end; suppose A34: q`1 q`2; (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p} proof let x be object such that A38: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p); now per cases by A11,A38,XBOOLE_0:def 3; case A39: x in LSeg(p,v) /\ LSeg(p1,p); p in {q1: q1`2=p`2 & p1`1<=q1`1 & q1`1<=v`1} by A32,A36; then p in LSeg(p1,v) by A9,A15,A32,A35,Th10,XXREAL_0:2; hence thesis by A39,TOPREAL1:8; end; case A40: x in LSeg(v,q) /\ LSeg(p1,p); then x in LSeg(v,q) by XBOOLE_0:def 4; then x in {p2: p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2} by A12,A37 ,Th9; then A41: ex p2 st p2=x & p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2; x in LSeg(p1, p) by A40,XBOOLE_0:def 4; then x in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A9,A13 ,A32,Th10; then ex q2 st q2=x & q2`2=p`2 & p1 `1<=q2`1 & q2`1<=p`1; hence contradiction by A35,A41; end; end; hence thesis; end; hence thesis by A10; end; suppose A42: p`2