let p, q be Point of (TOP-REAL 2); :: thesis: ( p `1 <> q `1 & p `2 = q `2 implies |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in LSeg p,q )
set p1 = |[(((p `1 ) + (q `1 )) / 2),(p `2 )]|;
assume that
A1: p `1 <> q `1 and
A2: p `2 = q `2 ; :: thesis: |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in LSeg p,q
A3: ( p = |[(p `1 ),(p `2 )]| & q = |[(q `1 ),(p `2 )]| ) by A2, EUCLID:57;
A4: ( |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| `1 = ((p `1 ) + (q `1 )) / 2 & |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| `2 = p `2 ) by EUCLID:56;

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

suppose A5: p `1 < q `1 ; :: thesis: |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in LSeg p,q

then ( p `1 <= ((p `1 ) + (q `1 )) / 2 & ((p `1 ) + (q `1 )) / 2 <= q `1 ) by XREAL_1:228;
then |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A4;
hence |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in LSeg p,q by A3, A5, Th16; :: thesis: verum

end;

suppose A6: p `1 > q `1 ; :: thesis: |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in LSeg p,q

then ( q `1 <= ((p `1 ) + (q `1 )) / 2 & ((p `1 ) + (q `1 )) / 2 <= p `1 ) by XREAL_1:228;
then |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) } by A4;
hence |[(((p `1 ) + (q `1 )) / 2),(p `2 )]| in LSeg p,q by A3, A6, Th16; :: thesis: verum

end;

end;