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