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 :: thesis: for a being Element of G st a in gr (A /\ B) holds
a in (gr A) /\ (gr B)

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 and
A2: rng F c= A /\ B and
A3: Product (F |^ I) = a by Th28;
A /\ B c= B by XBOOLE_1:17;
then rng F c= B by A2;
then A4: a in gr B by A1, A3, Th28;
A /\ B c= A by XBOOLE_1:17;
then rng F c= A by A2;
then a in gr A by A1, A3, Th28;
hence a in (gr A) /\ (gr B) by A4, GROUP_2:82; :: thesis: verum

end;

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