consider p being Point of ;
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