for G, H being Group holds (1). G, (1). H are_isomorphic by Th69;