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

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

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

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

end;

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

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

end;

end;