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
A1: ( the carrier of (X /\ Y) = (carr X) /\ (carr Y) & the carrier of (X /\ Y) = (carr X) /\ (carr Y) & carr X = the carrier of X & the carrier of Y = carr Y & carr X = the carrier of X & the carrier of Y = carr Y ) by GROUP_2:def 10;
reconsider Z = X /\ Y as Subgroup of G by GROUP_2:65;
X /\ Y = Z by A1, GROUP_2:97;
hence X /\ Y = X /\ Y ; :: thesis: verum