thus Segm n is with_zero ; :: thesis: verum