let p1, p, q be Point of (TOP-REAL 2); :: thesis: for r being real number
for u being Point of (Euclid 2) st not p1 in Ball u,r & p in Ball u,r & |[(q `1 ),(p `2 )]| in Ball u,r & not |[(q `1 ),(p `2 )]| in LSeg p1,p & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds
((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p}
let r be real number ; :: thesis: for u being Point of (Euclid 2) st not p1 in Ball u,r & p in Ball u,r & |[(q `1 ),(p `2 )]| in Ball u,r & not |[(q `1 ),(p `2 )]| in LSeg p1,p & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds
((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p}
let u be Point of (Euclid 2); :: thesis: ( not p1 in Ball u,r & p in Ball u,r & |[(q `1 ),(p `2 )]| in Ball u,r & not |[(q `1 ),(p `2 )]| in LSeg p1,p & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 implies ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p} )
set v = |[(q `1 ),(p `2 )]|;
assume that
A1: not p1 in Ball u,r and
A2: p in Ball u,r and
A3: |[(q `1 ),(p `2 )]| in Ball u,r and
A4: not |[(q `1 ),(p `2 )]| in LSeg p1,p and
A5: p1 `2 = p `2 and
A6: p `1 <> q `1 and
A7: p `2 <> q `2 ; :: thesis: ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p}
A8: LSeg p,|[(q `1 ),(p `2 )]| c= Ball u,r by A2, A3, Th28;
A9: p1 = |[(p1 `1 ),(p `2 )]| by A5, EUCLID:57;
p in LSeg p,|[(q `1 ),(p `2 )]| by RLTOPSP1:69;
then ( p in LSeg p1,p & p in (LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q) ) by RLTOPSP1:69, XBOOLE_0:def 3;
then p in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) by XBOOLE_0:def 4;
then A10: {p} c= ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) by ZFMISC_1:37;
A11: ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = ((LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg p1,p)) \/ ((LSeg |[(q `1 ),(p `2 )]|,q) /\ (LSeg p1,p)) by XBOOLE_1:23;
A12: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
A13: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A14: |[(q `1 ),(p `2 )]| `2 = p `2 by EUCLID:56;
A15: |[(q `1 ),(p `2 )]| `1 = q `1 by EUCLID:56;

per cases ( p1 `1 = p `1 or p1 `1 <> p `1 ) ;

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

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

end;

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

now

per cases ( p1 `1 > p `1 or p1 `1 < p `1 ) by A16, XXREAL_0:1;

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

now

per cases ( p `1 > q `1 or p `1 < q `1 ) by A6, XXREAL_0:1;

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

then A19: p `1 >= |[(q `1 ),(p `2 )]| `1 by EUCLID:56;

now

per cases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1;

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

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

proof

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

now

per cases ( x in (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg p1,p) or x in (LSeg |[(q `1 ),(p `2 )]|,q) /\ (LSeg p1,p) ) by A11, A21, XBOOLE_0:def 3;

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

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

end;

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

then x in LSeg q,|[(q `1 ),(p `2 )]| by XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A20, Th15;
then A24: ex p2 being Point of (TOP-REAL 2) 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 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th16;
then ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ;
hence contradiction by A18, A24; :: thesis: verum

end;

end;

end;

hence x in {p} ; :: thesis: verum

end;

hence ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p} by A10, XBOOLE_0:def 10; :: thesis: verum

end;

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

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) or x in {p} )
assume A26: x in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) ; :: thesis: x in {p}

now

per cases ( x in (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg p1,p) or x in (LSeg |[(q `1 ),(p `2 )]|,q) /\ (LSeg p1,p) ) by A11, A26, XBOOLE_0:def 3;

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

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & |[(q `1 ),(p `2 )]| `1 <= q1 `1 & q1 `1 <= p1 `1 ) } by A17, A19;
then p in LSeg p1,|[(q `1 ),(p `2 )]| by A9, A15, A17, A18, Th16, XXREAL_0:2;
hence x in {p} by A27, TOPREAL1:14; :: thesis: verum

end;

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

then x in LSeg p1,p by XBOOLE_0:def 4;
then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th16;
then A29: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ;
x in LSeg |[(q `1 ),(p `2 )]|,q by A28, XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1 ),(p `2 )]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A25, Th15;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = q `1 & |[(q `1 ),(p `2 )]| `2 <= p2 `2 & p2 `2 <= q `2 ) ;
hence contradiction by A18, A29; :: thesis: verum

end;

end;

end;

hence x in {p} ; :: thesis: verum

end;

hence ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p} by A10, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

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

end;

case A30: p `1 < q `1 ; :: thesis: contradiction

now

per cases ( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 ) by XXREAL_0:1;

suppose A31: q `1 > p1 `1 ; :: thesis: contradiction

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

end;

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

hence contradiction by A1, A3, A5, EUCLID:57; :: thesis: verum

end;

suppose q `1 < p1 `1 ; :: thesis: contradiction

then |[(q `1 ),(p `2 )]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= p1 `1 ) } by A15, A14, A30;
hence contradiction by A4, A9, A13, A17, Th16; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

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

end;

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

now

per cases ( p `1 > q `1 or p `1 < q `1 ) by A6, XXREAL_0:1;

case A33: p `1 > q `1 ; :: thesis: contradiction

now

per cases ( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 ) by XXREAL_0:1;

suppose q `1 > p1 `1 ; :: thesis: contradiction

then |[(q `1 ),(p `2 )]| in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A15, A14, A33;
hence contradiction by A4, A9, A13, A32, Th16; :: thesis: verum

end;

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

hence contradiction by A1, A3, A5, EUCLID:57; :: thesis: verum

end;

suppose A34: q `1 < p1 `1 ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then A36: p `1 <= |[(q `1 ),(p `2 )]| `1 by EUCLID:56;

now

per cases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1;

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

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) or x in {p} )
assume A38: x in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) ; :: thesis: x in {p}

now

per cases ( x in (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg p1,p) or x in (LSeg |[(q `1 ),(p `2 )]|,q) /\ (LSeg p1,p) ) by A11, A38, XBOOLE_0:def 3;

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

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & p1 `1 <= q1 `1 & q1 `1 <= |[(q `1 ),(p `2 )]| `1 ) } by A32, A36;
then p in LSeg p1,|[(q `1 ),(p `2 )]| by A9, A15, A32, A35, Th16, XXREAL_0:2;
hence x in {p} by A39, TOPREAL1:14; :: thesis: verum

end;

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

then x in LSeg |[(q `1 ),(p `2 )]|,q by XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A37, Th15;
then A41: ex p2 being Point of (TOP-REAL 2) 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 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th16;
then ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ;
hence contradiction by A35, A41; :: thesis: verum

end;

end;

end;

hence x in {p} ; :: thesis: verum

end;

hence ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p} by A10, XBOOLE_0:def 10; :: thesis: verum

end;

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

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) or x in {p} )
assume A43: x in ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) ; :: thesis: x in {p}

now

per cases ( x in (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg p1,p) or x in (LSeg |[(q `1 ),(p `2 )]|,q) /\ (LSeg p1,p) ) by A11, A43, XBOOLE_0:def 3;

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

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & p1 `1 <= q1 `1 & q1 `1 <= |[(q `1 ),(p `2 )]| `1 ) } by A32, A36;
then p in LSeg p1,|[(q `1 ),(p `2 )]| by A9, A15, A32, A35, Th16, XXREAL_0:2;
hence x in {p} by A44, TOPREAL1:14; :: thesis: verum

end;

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

then x in LSeg p1,p by XBOOLE_0:def 4;
then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th16;
then A46: ex q2 being Point of (TOP-REAL 2) st
( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ;
x in LSeg |[(q `1 ),(p `2 )]|,q by A45, XBOOLE_0:def 4;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1 ),(p `2 )]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A42, Th15;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = q `1 & |[(q `1 ),(p `2 )]| `2 <= p2 `2 & p2 `2 <= q `2 ) ;
hence contradiction by A35, A46; :: thesis: verum

end;

end;

end;

hence x in {p} ; :: thesis: verum

end;

hence ((LSeg p,|[(q `1 ),(p `2 )]|) \/ (LSeg |[(q `1 ),(p `2 )]|,q)) /\ (LSeg p1,p) = {p} by A10, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

end;