let p, q be Point of (TOP-REAL 2); :: thesis: ( p `1 <> q `1 & p `2 = q `2 implies (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|} )
assume that
A1: p `1 <> q `1 and
A2: p `2 = q `2 ; :: thesis: (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|}
set p3 = |[(((p `1) + (q `1)) / 2),(p `2)]|;
set l23 = LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|);
set l = LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q);
thus (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) c= {|[(((p `1) + (q `1)) / 2),(p `2)]|} :: according to XBOOLE_0:def 10 :: thesis: {|[(((p `1) + (q `1)) / 2),(p `2)]|} c= (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) or x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} )
A3: LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) = LSeg (|[(p `1),(p `2)]|,|[(((p `1) + (q `1)) / 2),(p `2)]|) by EUCLID:53;
assume A4: x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) ; :: thesis: x in {|[(((p `1) + (q `1)) / 2),(p `2)]|}
then A5: x in LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) by XBOOLE_0:def 4;
A6: LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) = LSeg (|[(((p `1) + (q `1)) / 2),(q `2)]|,|[(q `1),(q `2)]|) by A2, EUCLID:53;
A7: x in LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) by A4, XBOOLE_0:def 4;

now :: thesis: x = |[(((p `1) + (q `1)) / 2),(p `2)]|

per cases ( p `1 < q `1 or p `1 > q `1 ) by A1, XXREAL_0:1;

suppose A8: p `1 < q `1 ; :: thesis: x = |[(((p `1) + (q `1)) / 2),(p `2)]|

then p `1 < ((p `1) + (q `1)) / 2 by XREAL_1:226;
then x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = p `2 & p `1 <= p1 `1 & p1 `1 <= ((p `1) + (q `1)) / 2 ) } by A7, A3, Th10;
then consider t1 being Point of (TOP-REAL 2) such that
A9: t1 = x and
A10: t1 `2 = p `2 and
p `1 <= t1 `1 and
A11: t1 `1 <= ((p `1) + (q `1)) / 2 ;
A12: t1 `1 <= |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A11;
((p `1) + (q `1)) / 2 < q `1 by A8, XREAL_1:226;
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & ((p `1) + (q `1)) / 2 <= p2 `1 & p2 `1 <= q `1 ) } by A5, A6, Th10;
then ex t2 being Point of (TOP-REAL 2) st
( t2 = x & t2 `2 = q `2 & ((p `1) + (q `1)) / 2 <= t2 `1 & t2 `1 <= q `1 ) ;
then t1 `1 >= |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A9;
then A13: t1 `1 = |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A12, XXREAL_0:1;
t1 `2 = |[(((p `1) + (q `1)) / 2),(p `2)]| `2 by A10;
hence x = |[(((p `1) + (q `1)) / 2),(p `2)]| by A9, A13, Th6; :: thesis: verum

end;

suppose A14: p `1 > q `1 ; :: thesis: x = |[(((p `1) + (q `1)) / 2),(p `2)]|

then p `1 > ((p `1) + (q `1)) / 2 by XREAL_1:226;
then x in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & ((p `1) + (q `1)) / 2 <= p11 `1 & p11 `1 <= p `1 ) } by A7, A3, Th10;
then consider t1 being Point of (TOP-REAL 2) such that
A15: t1 = x and
A16: t1 `2 = p `2 and
A17: ((p `1) + (q `1)) / 2 <= t1 `1 and
t1 `1 <= p `1 ;
A18: |[(((p `1) + (q `1)) / 2),(p `2)]| `1 <= t1 `1 by A17;
q `1 < ((p `1) + (q `1)) / 2 by A14, XREAL_1:226;
then x in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = q `2 & q `1 <= p22 `1 & p22 `1 <= ((p `1) + (q `1)) / 2 ) } by A5, A6, Th10;
then ex t2 being Point of (TOP-REAL 2) st
( t2 = x & t2 `2 = q `2 & q `1 <= t2 `1 & t2 `1 <= ((p `1) + (q `1)) / 2 ) ;
then t1 `1 <= |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A15;
then A19: t1 `1 = |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A18, XXREAL_0:1;
t1 `2 = |[(((p `1) + (q `1)) / 2),(p `2)]| `2 by A16;
hence x = |[(((p `1) + (q `1)) / 2),(p `2)]| by A15, A19, Th6; :: thesis: verum

end;

end;

end;

hence x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} by TARSKI:def 1; :: thesis: verum

end;

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