take (Segm the Nat) --> 1 ; :: thesis: ( (Segm the Nat) --> 1 is natural-valued & (Segm the Nat) --> 1 is positive-yielding )
thus ( (Segm the Nat) --> 1 is natural-valued & (Segm the Nat) --> 1 is positive-yielding ) ; :: thesis: verum