let G be Group; :: thesis: for A being Subgroup of G
for X, Y being Subgroup of A holds X /\ Y = X /\ Y
let A be Subgroup of G; :: thesis: for X, Y being Subgroup of A holds X /\ Y = X /\ Y
let X, Y be Subgroup of A; :: thesis: X /\ Y = X /\ Y
reconsider Z = X /\ Y as Subgroup of G by GROUP_2:56;
the carrier of (X /\ Y) = (carr X) /\ (carr Y) by GROUP_2:def 10;
then X /\ Y = Z by GROUP_2:80;
hence X /\ Y = X /\ Y ; :: thesis: verum