theorem :: GROUP_10:16

for n being non zero Nat holds card (INT.Group n) = n by Lm1;