take NulForm V,V ; :: thesis: NulForm V,V is alternating
thus NulForm V,V is alternating ; :: thesis: verum