consider p being Point of (TOP-REAL 2);
take LSeg (p,p) ; :: thesis: ( LSeg (p,p) is convex & not LSeg (p,p) is empty )
thus ( LSeg (p,p) is convex & not LSeg (p,p) is empty ) ; :: thesis: verum