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

consider x being 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 x in LSeg |[(p2 `1 ),(p `2 )]|,p by XBOOLE_0:def 4;
then consider s1 being Real such that
A5: x = ((1 - s1) * |[(p2 `1 ),(p `2 )]|) + (s1 * p) and
0 <= s1 and
s1 <= 1 ;
x in LSeg q,p2 by A4, XBOOLE_0:def 4;
then consider s2 being Real such that
A6: x = ((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 Th7
.= ((1 - s1) * (|[(p2 `1 ),(p `2 )]| `2 )) + ((s1 * p) `2 ) by Th9
.= ((1 - s1) * (|[(p2 `1 ),(p `2 )]| `2 )) + (s1 * (p `2 )) by Th9
.= ((1 - s1) * (p `2 )) + (s1 * (p `2 )) by EUCLID:56
.= p `2 ;
(((1 - s2) * q) + (s2 * p2)) `2 = (((1 - s2) * q) `2 ) + ((s2 * p2) `2 ) by Th7
.= ((1 - s2) * (q `2 )) + ((s2 * p2) `2 ) by Th9
.= ((1 - s2) * (q `2 )) + (s2 * (p2 `2 )) by Th9
.= 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 set ; :: 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 Th7
.= ((1 - s2) * (q `2 )) + ((s2 * p2) `2 ) by Th9
.= ((1 - s2) * (q `2 )) + (s2 * (p2 `2 )) by Th9
.= 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 Th7
.= ((1 - s1) * (p2 `1 )) + ((s1 * |[(p2 `1 ),(p `2 )]|) `1 ) by Th9
.= ((1 - s1) * (p2 `1 )) + (s1 * (|[(p2 `1 ),(p `2 )]| `1 )) by Th9
.= ((1 - s1) * (p2 `1 )) + (s1 * (p2 `1 )) by EUCLID:56
.= 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:57
.= p2 by A10, A13, A11, A12, EUCLID:57 ;
hence x in {p2} by A10, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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:69;
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