let q, p2, p be Point of (TOP-REAL 2); :: thesis: ( q `1 = p2 `1 & p `1 <> p2 `1 implies ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = {p2} )
assume that
A1: q `1 = p2 `1 and
A2: p `1 <> p2 `1 ; :: thesis: ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = {p2}
set p3 = |[(p `1),(p2 `2)]|;
set l23 = LSeg (p2,|[(p `1),(p2 `2)]|);
set l3 = LSeg (|[(p `1),(p2 `2)]|,p);
set l = LSeg (q,p2);
A3: (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) = {}

proof

set x = the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2));
assume A4: (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) <> {} ; :: thesis: contradiction
then the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (|[(p `1),(p2 `2)]|,p) by XBOOLE_0:def 4;
then consider d1 being Real such that
A5: the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - d1) * |[(p `1),(p2 `2)]|) + (d1 * p) and
0 <= d1 and
d1 <= 1 ;
the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (q,p2) by A4, XBOOLE_0:def 4;
then consider d2 being Real such that
A6: the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - d2) * q) + (d2 * p2) and
0 <= d2 and
d2 <= 1 ;
A7: (((1 - d1) * |[(p `1),(p2 `2)]|) + (d1 * p)) `1 = (((1 - d1) * |[(p `1),(p2 `2)]|) `1) + ((d1 * p) `1) by Th2
.= ((1 - d1) * (|[(p `1),(p2 `2)]| `1)) + ((d1 * p) `1) by Th4
.= ((1 - d1) * (|[(p `1),(p2 `2)]| `1)) + (d1 * (p `1)) by Th4
.= ((1 - d1) * (p `1)) + (d1 * (p `1))
.= p `1 ;
(((1 - d2) * q) + (d2 * p2)) `1 = (((1 - d2) * q) `1) + ((d2 * p2) `1) by Th2
.= ((1 - d2) * (q `1)) + ((d2 * p2) `1) by Th4
.= ((1 - d2) * (q `1)) + (d2 * (p2 `1)) by Th4
.= p2 `1 by A1 ;
hence contradiction by A2, A5, A7, A6; :: thesis: verum

end;

A8: (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) = {p2}

proof

thus (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) c= {p2} :: according to XBOOLE_0:def 10 :: thesis: {p2} c= (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) or x in {p2} )
assume A9: x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) ; :: thesis: x in {p2}
then x in LSeg (p2,|[(p `1),(p2 `2)]|) by XBOOLE_0:def 4;
then consider s1 being Real such that
A10: x = ((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|) and
0 <= s1 and
s1 <= 1 ;
x in LSeg (q,p2) by A9, XBOOLE_0:def 4;
then consider s2 being Real such that
A11: x = ((1 - s2) * q) + (s2 * p2) and
0 <= s2 and
s2 <= 1 ;
A12: (((1 - s2) * q) + (s2 * p2)) `1 = (((1 - s2) * q) `1) + ((s2 * p2) `1) by Th2
.= ((1 - s2) * (q `1)) + ((s2 * p2) `1) by Th4
.= ((1 - s2) * (q `1)) + (s2 * (p2 `1)) by Th4
.= p2 `1 by A1 ;
set t = ((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|);
A13: (((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|)) `2 = (((1 - s1) * p2) `2) + ((s1 * |[(p `1),(p2 `2)]|) `2) by Th2
.= ((1 - s1) * (p2 `2)) + ((s1 * |[(p `1),(p2 `2)]|) `2) by Th4
.= ((1 - s1) * (p2 `2)) + (s1 * (|[(p `1),(p2 `2)]| `2)) by Th4
.= ((1 - s1) * (p2 `2)) + (s1 * (p2 `2))
.= p2 `2 ;
((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|) = |[((((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|)) `1),((((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|)) `2)]| by EUCLID:53
.= p2 by A10, A13, A11, A12, EUCLID:53 ;
hence x in {p2} by A10, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {p2} or x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) )
assume x in {p2} ; :: thesis: x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2))
then A14: x = p2 by TARSKI:def 1;
( p2 in LSeg (p2,|[(p `1),(p2 `2)]|) & p2 in LSeg (q,p2) ) by RLTOPSP1:68;
hence x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) by A14, XBOOLE_0:def 4; :: thesis: verum

end;

thus ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = ((LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2))) \/ ((LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2))) by XBOOLE_1:23
.= {p2} by A8, A3 ; :: thesis: verum