theorem :: GROUP_1A:133

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