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

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