take 0_ G ; :: according to SETWISEO:def 2 :: thesis: 0_ G is_a_unity_wrt the addF of G
thus 0_ G is_a_unity_wrt the addF of G by Th20; :: thesis: verum