let G be Group; :: thesis: for H1, H2 being Subgroup of G holds
( H1 * H2 c= the carrier of (H1 "\/" H2) & H2 * H1 c= the carrier of (H1 "\/" H2) )
let H1, H2 be Subgroup of G; :: thesis: ( H1 * H2 c= the carrier of (H1 "\/" H2) & H2 * H1 c= the carrier of (H1 "\/" H2) )
thus H1 * H2 c= the carrier of (H1 "\/" H2) by Th61; :: thesis: H2 * H1 c= the carrier of (H1 "\/" H2)
H2 * H1 c= the carrier of (H2 "\/" H1) by Th61;
hence H2 * H1 c= the carrier of (H1 "\/" H2) by GROUP_4:56; :: thesis: verum