take 1 .--> 1 ; :: thesis: ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued )
thus ( not 1 .--> 1 is empty & 1 .--> 1 is constant & 1 .--> 1 is natural-valued ) ; :: thesis: verum