:: deftheorem Def11 defines are_isomorphic GROUP_6:def 11 :
for G, H being Group holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );