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