let G be Group; :: thesis: for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1 "\/" H2
let H1, H2 be Subgroup of G; :: thesis: H1 /\ H2 is Subgroup of H1 "\/" H2
( H1 /\ H2 is Subgroup of H1 & H1 is Subgroup of H1 "\/" H2 ) by Th60, GROUP_2:88;
hence H1 /\ H2 is Subgroup of H1 "\/" H2 by GROUP_2:56; :: thesis: verum