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