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

proof

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

end;

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

proof

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

proof

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

end;

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