let G be Group; :: thesis: for H1, H2 being Subgroup of G holds H1 /\ H2 is Subgroup of H1

let H1, H2 be Subgroup of G; :: thesis: H1 /\ H2 is Subgroup of H1

the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 by Th80;

hence H1 /\ H2 is Subgroup of H1 by Th57, XBOOLE_1:17; :: thesis: verum

let H1, H2 be Subgroup of G; :: thesis: H1 /\ H2 is Subgroup of H1

the carrier of (H1 /\ H2) = the carrier of H1 /\ the carrier of H2 by Th80;

hence H1 /\ H2 is Subgroup of H1 by Th57, XBOOLE_1:17; :: thesis: verum