let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G )
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G holds
( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G )
let H1 be StableSubgroup of G; :: thesis: ( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G )
the carrier of ((Omega). G) \/ (carr H1) = [#] the carrier of G by SUBSET_1:11;
hence ( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G ) by Th25; :: thesis: verum