for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G )