take id G ; :: thesis: id G is bijective
thus id G is bijective ; :: thesis: verum