take 1 ; :: according to GROUP_10:def 17 :: thesis: card (INT.Group p) = p |^ 1
thus card (INT.Group p) = p by Lm1
.= p |^ 1 ; :: thesis: verum