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

proof

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

end;

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