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

proof

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

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

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