assume the ZeroF of (Trivial-COM A) in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
hence contradiction by Def1; :: thesis: verum