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 object ; :: 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 Th2
.= ((1 - d1) * (p `2)) + ((d1 * |[(q `1),(p `2)]|) `2) by Th4
.= ((1 - d1) * (p `2)) + (d1 * (|[(q `1),(p `2)]| `2)) by Th4
.= ((1 - d1) * (|[(q `1),(p `2)]| `2)) + (d1 * (|[(q `1),(p `2)]| `2))
.= |[(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, Th2
.= ((1 - d2) * (|[(q `1),(p `2)]| `1)) + ((d2 * q) `1) by Th4
.= ((1 - d2) * (|[(q `1),(p `2)]| `1)) + (d2 * (q `1)) by Th4
.= ((1 - d2) * (|[(q `1),(p `2)]| `1)) + (d2 * (|[(q `1),(p `2)]| `1))
.= |[(q `1),(p `2)]| `1 ;
then ((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|) = |[(q `1),(p `2)]| by A4, Th6;
hence x in {|[(q `1),(p `2)]|} by A2, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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:68;
hence x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) by A5, XBOOLE_0:def 4; :: thesis: verum