n <> 0 ;
hence not Segm n is empty ; :: thesis: verum