set a = the Point of (TOP-REAL n);
take LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) ; :: thesis: ( not LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is empty & LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is convex )
thus ( not LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is empty & LSeg ( the Point of (TOP-REAL n), the Point of (TOP-REAL n)) is convex ) ; :: thesis: verum