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