for G being strict addGroup holds ((Omega). G) /\ ((Omega). G) = G by Lm3;