let G be Group; :: thesis: for H being Subgroup of G holds
( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )
let H be Subgroup of G; :: thesis: ( ((Omega). G) "\/" H = (Omega). G & H "\/" ((Omega). G) = (Omega). G )
A1: the carrier of ((Omega). G) \/ (carr H) = [#] the carrier of G by SUBSET_1:11;
hence ((Omega). G) "\/" H = (Omega). G by Th31; :: thesis: H "\/" ((Omega). G) = (Omega). G
thus H "\/" ((Omega). G) = (Omega). G by A1, Th31; :: thesis: verum