let G be Group; :: thesis: for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H
let H be Subgroup of G; :: thesis: ((Omega). G) /\ H = (Omega). H
A1: (Omega). H is strict Subgroup of G by GROUP_2:56;
the carrier of ((Omega). G) /\ the carrier of H = the carrier of ((Omega). H) by XBOOLE_1:28, GROUP_2:def 5;
hence ((Omega). G) /\ H = (Omega). H by A1, GROUP_2:80; :: thesis: verum