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