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