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 A1: ( p `1 = q `1 & 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)]|} )
assume 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 A2: ( x in LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| & x in LSeg |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q ) by XBOOLE_0:def 4;
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;
A4: 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;

now

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

suppose A5: 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 A2, A3, Th15;
then consider t1 being Point of (TOP-REAL 2) such that
A6: ( t1 = x & t1 `1 = p `1 & p `2 <= t1 `2 & t1 `2 <= ((p `2 ) + (q `2 )) / 2 ) ;
A7: t1 `2 <= |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `2 by A6, EUCLID:56;
((p `2 ) + (q `2 )) / 2 < q `2 by A5, 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 A2, A4, 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 A6, EUCLID:56;
then ( t1 `2 = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `2 & t1 `1 = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `1 ) by A6, A7, EUCLID:56, XXREAL_0:1;
hence x = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| by A6, Th11; :: thesis: verum

end;

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 { 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 A2, A3, Th15;
then consider t1 being Point of (TOP-REAL 2) such that
A9: ( t1 = x & t1 `1 = p `1 & ((p `2 ) + (q `2 )) / 2 <= t1 `2 & t1 `2 <= p `2 ) ;
A10: |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `2 <= t1 `2 by A9, EUCLID:56;
q `2 < ((p `2 ) + (q `2 )) / 2 by A8, 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 A2, A4, 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 A9, EUCLID:56;
then ( t1 `2 = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `2 & t1 `1 = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| `1 ) by A9, A10, EUCLID:56, XXREAL_0:1;
hence x = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| by A9, 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 ( x = |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]| & |[(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, TARSKI:def 1;
hence x in (LSeg p,|[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|) /\ (LSeg |[(p `1 ),(((p `2 ) + (q `2 )) / 2)]|,q) by XBOOLE_0:def 4; :: thesis: verum