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