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 set ; :: 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 Th7
.= ((1 - d1) * (p `1 )) + ((d1 * |[(p `1 ),(q `2 )]|) `1 ) by Th9
.= ((1 - d1) * (p `1 )) + (d1 * (|[(p `1 ),(q `2 )]| `1 )) by Th9
.= ((1 - d1) * (p `1 )) + (d1 * (p `1 )) by EUCLID:56
.= |[(p `1 ),(q `2 )]| `1 by EUCLID:56 ;
(((1 - d1) * p) + (d1 * |[(p `1 ),(q `2 )]|)) `2 = (((1 - d2) * |[(p `1 ),(q `2 )]|) `2 ) + ((d2 * q) `2 ) by A2, A3, Th7
.= ((1 - d2) * (|[(p `1 ),(q `2 )]| `2 )) + ((d2 * q) `2 ) by Th9
.= ((1 - d2) * (|[(p `1 ),(q `2 )]| `2 )) + (d2 * (q `2 )) by Th9
.= ((1 - d2) * (q `2 )) + (d2 * (q `2 )) by EUCLID:56
.= |[(p `1 ),(q `2 )]| `2 by EUCLID:56 ;
then ((1 - d1) * p) + (d1 * |[(p `1 ),(q `2 )]|) = |[(p `1 ),(q `2 )]| by A4, Th11;
hence x in {|[(p `1 ),(q `2 )]|} by A2, TARSKI:def 1; :: thesis: verum

end;

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