let p, q be Point of (TOP-REAL 2); :: thesis: (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg |[(q `1 ),(p `2 )]|,q) = {|[(q `1 ),(p `2 )]|}
set p3 = |[(q `1 ),(p `2 )]|;
set l23 = LSeg p,|[(q `1 ),(p `2 )]|;
set l = LSeg |[(q `1 ),(p `2 )]|,q;
thus (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg |[(q `1 ),(p `2 )]|,q) c= {|[(q `1 ),(p `2 )]|} :: according to XBOOLE_0:def 10 :: thesis: {|[(q `1 ),(p `2 )]|} c= (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg |[(q `1 ),(p `2 )]|,q)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg |[(q `1 ),(p `2 )]|,q) or x in {|[(q `1 ),(p `2 )]|} )
assume A1: x in (LSeg p,|[(q `1 ),(p `2 )]|) /\ (LSeg |[(q `1 ),(p `2 )]|,q) ; :: thesis: x in {|[(q `1 ),(p `2 )]|}
then x in LSeg p,|[(q `1 ),(p `2 )]| by XBOOLE_0:def 4;
then consider d1 being Real such that
A2: x = ((1 - d1) * p) + (d1 * |[(q `1 ),(p `2 )]|) and
0 <= d1 and
d1 <= 1 ;
x in LSeg |[(q `1 ),(p `2 )]|,q by A1, XBOOLE_0:def 4;
then consider d2 being Real such that
A3: x = ((1 - d2) * |[(q `1 ),(p `2 )]|) + (d2 * q) and
0 <= d2 and
d2 <= 1 ;
set t = ((1 - d1) * p) + (d1 * |[(q `1 ),(p `2 )]|);
A4: (((1 - d1) * p) + (d1 * |[(q `1 ),(p `2 )]|)) `2 = (((1 - d1) * p) `2 ) + ((d1 * |[(q `1 ),(p `2 )]|) `2 ) by Th7
.= ((1 - d1) * (p `2 )) + ((d1 * |[(q `1 ),(p `2 )]|) `2 ) by Th9
.= ((1 - d1) * (p `2 )) + (d1 * (|[(q `1 ),(p `2 )]| `2 )) by Th9
.= ((1 - d1) * (|[(q `1 ),(p `2 )]| `2 )) + (d1 * (|[(q `1 ),(p `2 )]| `2 )) by EUCLID:56
.= |[(q `1 ),(p `2 )]| `2 ;
(((1 - d1) * p) + (d1 * |[(q `1 ),(p `2 )]|)) `1 = (((1 - d2) * |[(q `1 ),(p `2 )]|) `1 ) + ((d2 * q) `1 ) by A2, A3, Th7
.= ((1 - d2) * (|[(q `1 ),(p `2 )]| `1 )) + ((d2 * q) `1 ) by Th9
.= ((1 - d2) * (|[(q `1 ),(p `2 )]| `1 )) + (d2 * (q `1 )) by Th9
.= ((1 - d2) * (|[(q `1 ),(p `2 )]| `1 )) + (d2 * (|[(q `1 ),(p `2 )]| `1 )) by EUCLID:56
.= |[(q `1 ),(p `2 )]| `1 ;
then ((1 - d1) * p) + (d1 * |[(q `1 ),(p `2 )]|) = |[(q `1 ),(p `2 )]| by A4, Th11;
hence x in {|[(q `1 ),(p `2 )]|} by A2, TARSKI:def 1; :: thesis: verum

end;

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