let p, q be Point of (TOP-REAL 2); :: thesis: LSeg p,q is convex
for w1, w2 being Point of (TOP-REAL 2) st w1 in LSeg p,q & w2 in LSeg p,q holds
LSeg w1,w2 c= LSeg p,q by TOPREAL1:12;
hence LSeg p,q is convex by JORDAN1:def 1; :: thesis: verum