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