let G be Group; :: thesis: for H being strict Subgroup of G holds H /\ H = H
let H be strict Subgroup of G; :: thesis: H /\ H = H
the carrier of (H /\ H) = (carr H) /\ (carr H) by Def10
.= the carrier of H ;
hence H /\ H = H by Th59; :: thesis: verum