let G be Group; :: thesis: for A, B being Subset of G holds gr (A /\ B) is Subgroup of (gr A) /\ (gr B)
let A, B be Subset of G; :: thesis: gr (A /\ B) is Subgroup of (gr A) /\ (gr B)

now

let a be Element of G; :: thesis: ( a in gr (A /\ B) implies a in (gr A) /\ (gr B) )
assume a in gr (A /\ B) ; :: thesis: a in (gr A) /\ (gr B)
then consider F being FinSequence of the carrier of G, I being FinSequence of INT such that
A1: ( len F = len I & rng F c= A /\ B & Product (F |^ I) = a ) by Th37;
( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
then ( rng F c= A & rng F c= B ) by A1, XBOOLE_1:1;
then ( a in gr A & a in gr B ) by A1, Th37;
hence a in (gr A) /\ (gr B) by GROUP_2:99; :: thesis: verum

end;

hence gr (A /\ B) is Subgroup of (gr A) /\ (gr B) by GROUP_2:67; :: thesis: verum