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