let G be Group; :: thesis: for H2 being Subgroup of G
for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
let H2 be Subgroup of G; :: thesis: for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1
let H1 be strict Subgroup of G; :: thesis: H1 /\ (H1 "\/" H2) = H1
H1 is Subgroup of H1 "\/" H2 by Th60;
hence H1 /\ (H1 "\/" H2) = H1 by GROUP_2:89; :: thesis: verum