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