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