let p, p1, q be Point of (TOP-REAL 2); :: thesis: for r being Real
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; :: 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, Th21;
A9: p1 = |[(p1 `1),(p `2)]| by A5, EUCLID:53;
p in LSeg (p,|[(q `1),(p `2)]|) by RLTOPSP1:68;
then ( p in LSeg (p1,p) & p in (LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) ) by RLTOPSP1:68, 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:31;
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:53;
A13: p = |[(p `1),(p `2)]| by EUCLID:53;
A14: |[(q `1),(p `2)]| `2 = p `2 ;
A15: |[(q `1),(p `2)]| `1 = q `1 ;

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, Th6; :: 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 :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

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 :: thesis: ( ( p `1 > q `1 & ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ) or ( p `1 < q `1 & contradiction ) )

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 ;

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

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 object ; :: 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 :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )

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, A17, A18, Th10, XXREAL_0:2;
hence x in {p} by A22, TOPREAL1:8; :: 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, Th9;
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, Th10;
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; :: 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 object ; :: 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 :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )

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, A17, A18, Th10, XXREAL_0:2;
hence x in {p} by A27, TOPREAL1:8; :: 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, Th10;
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, A25, Th9;
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; :: 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 :: thesis: contradiction

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, A17;
then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A17, A31, Th10, 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:53; :: 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, Th10; :: 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 :: thesis: ( ( p `1 > q `1 & contradiction ) or ( p `1 < q `1 & ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ) )

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 :: thesis: contradiction

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, Th10; :: thesis: verum

end;

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

hence contradiction by A1, A3, A5, EUCLID:53; :: 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, A32;
then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A32, A34, Th10, 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 ;

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

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 object ; :: 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 :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )

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, A32, A35, Th10, XXREAL_0:2;
hence x in {p} by A39, TOPREAL1:8; :: 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, Th9;
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, Th10;
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; :: 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 object ; :: 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 :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )

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, A32, A35, Th10, XXREAL_0:2;
hence x in {p} by A44, TOPREAL1:8; :: 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, Th10;
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, A42, Th9;
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; :: 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;