for p being Prime
for a, b being Element of (Z/Z* p)
for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})