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

now

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