take 1: (G1,G2) ; :: thesis: 1: (G1,G2) is constant
thus 1: (G1,G2) is constant ; :: thesis: verum