theorem :: GR_CY_1:23

INT.Group = gr {(@' 1)} by Lm5;