let G be Group; :: thesis: for H1, H2 being Subgroup of G holds H1 * H2 c= the carrier of (H1 "\/" H2)
let H1, H2 be Subgroup of G; :: thesis: H1 * H2 c= the carrier of (H1 "\/" H2)
H1 "\/" H2 = gr (H1 * H2) by GROUP_4:50;
hence H1 * H2 c= the carrier of (H1 "\/" H2) by GROUP_4:def 4; :: thesis: verum