take 1_ G ; :: thesis: 1_ G is unital
thus 1_ G = 1_ G ; :: according to TOPALG_7:def 1 :: thesis: verum