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 set ; :: 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:57;
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:57;
A7: x in LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| by A4, XBOOLE_0:def 4;

now

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:228;
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, Th15;
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, EUCLID:56;
((p `2 ) + (q `2 )) / 2 < q `2 by A8, XREAL_1:228;
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, Th15;
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, EUCLID:56;
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, EUCLID:56;
hence x = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| by A9, A13, Th11; :: 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:228;
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, Th15;
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, EUCLID:56;
q `2 < ((p `2 ) + (q `2 )) / 2 by A14, XREAL_1:228;
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, Th15;
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, EUCLID:56;
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, EUCLID:56;
hence x = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| by A15, A19, Th11; :: 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 set ; :: 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:69;
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