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