take 1 ; :: thesis: ( not 1 is zero & 1 is natural )
thus ( not 1 is zero & 1 is natural ) ; :: thesis: verum