let p1, q, p 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 & q in Ball u,r & p in Ball u,r & not p in LSeg p1,q & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) holds
(LSeg p1,q) /\ (LSeg q,p) = {q}
let r be real number ; :: thesis: for u being Point of (Euclid 2) st not p1 in Ball u,r & q in Ball u,r & p in Ball u,r & not p in LSeg p1,q & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) holds
(LSeg p1,q) /\ (LSeg q,p) = {q}
let u be Point of (Euclid 2); :: thesis: ( not p1 in Ball u,r & q in Ball u,r & p in Ball u,r & not p in LSeg p1,q & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) implies (LSeg p1,q) /\ (LSeg q,p) = {q} )
assume A1: ( not p1 in Ball u,r & q in Ball u,r & p in Ball u,r & not p in LSeg p1,q ) ; :: thesis: ( ( not ( q `1 = p `1 & q `2 <> p `2 ) & not ( q `1 <> p `1 & q `2 = p `2 ) ) or ( not p1 `1 = q `1 & not p1 `2 = q `2 ) or (LSeg p1,q) /\ (LSeg q,p) = {q} )
assume A2: ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) ; :: thesis: ( ( not p1 `1 = q `1 & not p1 `2 = q `2 ) or (LSeg p1,q) /\ (LSeg q,p) = {q} )
assume A3: ( p1 `1 = q `1 or p1 `2 = q `2 ) ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

A4: now

per cases ( p1 `1 = q `1 or p1 `2 = q `2 ) by A3;

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

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

end;

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

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

end;

end;

end;

A5: ( p = |[(p `1 ),(p `2 )]| & p1 = |[(p1 `1 ),(p1 `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;
A6: LSeg p,q c= Ball u,r by A1, Th28;

now

per cases ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) by A2;

suppose A7: ( q `1 = p `1 & q `2 <> p `2 ) ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

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

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

suppose A8: q `2 > p `2 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

per cases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A4;

suppose A9: ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

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

case p1 `2 > q `2 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

then ( q in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = p `1 & p `2 <= p11 `2 & p11 `2 <= p1 `2 ) } & p1 `2 > p `2 ) by A7, A8, XXREAL_0:2;
then q in LSeg p,p1 by A5, A7, A9, Th15;
hence (LSeg p1,q) /\ (LSeg q,p) = {q} by TOPREAL1:14; :: thesis: verum

end;

case A10: p1 `2 < q `2 ; :: thesis: contradiction

now

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

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

then ( p1 in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= q `2 ) } & p `2 < q `2 ) by A7, A9, A10, XXREAL_0:2;
then p1 in LSeg p,q by A5, A7, Th15;
hence contradiction by A1, A6; :: thesis: verum

end;

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

hence contradiction by A1, A7, A9, Th11; :: thesis: verum

end;

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

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 A8;
hence contradiction by A1, A5, A7, A9, A10, Th15; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

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

end;

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

hence (LSeg p1,q) /\ (LSeg q,p) = {q} by A5, A7, Th37; :: thesis: verum

end;

end;

end;

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

end;

suppose A11: q `2 < p `2 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

per cases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A4;

suppose A12: ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

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

case A13: p1 `2 > q `2 ; :: thesis: contradiction

now

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

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

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 A11;
hence contradiction by A1, A5, A7, A12, A13, Th15; :: thesis: verum

end;

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

hence contradiction by A1, A7, A12, Th11; :: thesis: verum

end;

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

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 A7, A12, A13;
then p1 in LSeg p,q by A5, A7, A11, Th15;
hence contradiction by A1, A6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case p1 `2 < q `2 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

then ( q in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = p `1 & p1 `2 <= p22 `2 & p22 `2 <= p `2 ) } & p1 `2 < p `2 ) by A7, A11, XXREAL_0:2;
then q in LSeg p1,p by A5, A7, A12, Th15;
hence (LSeg p1,q) /\ (LSeg q,p) = {q} by TOPREAL1:14; :: thesis: verum

end;

end;

end;

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

end;

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

hence (LSeg p1,q) /\ (LSeg q,p) = {q} by A5, A7, Th37; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

suppose A14: ( q `1 <> p `1 & q `2 = p `2 ) ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

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 ) } ;

now

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

suppose A15: q `1 > p `1 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

per cases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A4;

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

hence (LSeg p1,q) /\ (LSeg q,p) = {q} by A5, A14, Th36; :: thesis: verum

end;

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

now

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

case p1 `1 > q `1 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

then ( q in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & p `1 <= p11 `1 & p11 `1 <= p1 `1 ) } & p1 `1 > p `1 ) by A14, A15, XXREAL_0:2;
then q in LSeg p,p1 by A5, A14, A16, Th16;
hence (LSeg p1,q) /\ (LSeg q,p) = {q} by TOPREAL1:14; :: thesis: verum

end;

case A17: p1 `1 < q `1 ; :: thesis: contradiction

now

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

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

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

end;

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

hence contradiction by A1, A14, A16, Th11; :: thesis: verum

end;

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

then p in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= q `1 ) } by A15;
hence contradiction by A1, A5, A14, A16, A17, Th16; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

suppose A18: q `1 < p `1 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

per cases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A4;

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

hence (LSeg p1,q) /\ (LSeg q,p) = {q} by A5, A14, Th36; :: thesis: verum

end;

suppose A19: ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

now

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

case A20: p1 `1 > q `1 ; :: thesis: contradiction

now

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

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

then p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & q `1 <= q1 `1 & q1 `1 <= p1 `1 ) } by A18;
hence contradiction by A1, A5, A14, A19, A20, Th16; :: thesis: verum

end;

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

hence contradiction by A1, A14, A19, Th11; :: thesis: verum

end;

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

then p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = p `2 & q `1 <= p3 `1 & p3 `1 <= p `1 ) } by A14, A19, A20;
then p1 in LSeg p,q by A5, A14, A18, Th16;
hence contradiction by A1, A6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case p1 `1 < q `1 ; :: thesis: (LSeg p1,q) /\ (LSeg q,p) = {q}

then ( q in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = p `2 & p1 `1 <= p22 `1 & p22 `1 <= p `1 ) } & p1 `1 < p `1 ) by A14, A18, XXREAL_0:2;
then q in LSeg p1,p by A5, A14, A19, Th16;
hence (LSeg p1,q) /\ (LSeg q,p) = {q} by TOPREAL1:14; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

end;

end;

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