for G, H being strict Group st G,H are_isomorphic holds
card G = card H by Th73;