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