let C be Curve of T; :: thesis: ( C is with_last_point implies not C is empty )
assume ( C is with_last_point & C is empty ) ; :: thesis: contradiction
then reconsider c = {} as with_last_point Curve of T ;
dom c is right_end ;
hence contradiction ; :: thesis: verum