let G be Group; :: thesis: for H1, H2 being Subgroup of G holds H1 is Subgroup of H1 "\/" H2
let H1, H2 be Subgroup of G; :: thesis: H1 is Subgroup of H1 "\/" H2
( carr H1 c= (carr H1) \/ (carr H2) & (carr H1) \/ (carr H2) c= the carrier of (gr ((carr H1) \/ (carr H2))) ) by Def4, XBOOLE_1:7;
hence H1 is Subgroup of H1 "\/" H2 by GROUP_2:57, XBOOLE_1:1; :: thesis: verum