take 1 ; :: thesis: not 1 is zero
thus not 1 is zero ; :: thesis: verum