theorem :: GR_FREE0:72

for G, H being Group st G,H are_isomorphic holds
( G is free iff H is free ) by GROUP_6:67;