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