theorem :: GROUP_2:87

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