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

H1 /\ H3 is Subgroup of H2 /\ H3

let H1, H2, H3 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3 )

assume H1 is Subgroup of H2 ; :: thesis: H1 /\ H3 is Subgroup of H2 /\ H3

then the carrier of H1 c= the carrier of H2 by Def5;

then the carrier of H1 /\ the carrier of H3 c= the carrier of H2 /\ the carrier of H3 by XBOOLE_1:26;

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

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

hence H1 /\ H3 is Subgroup of H2 /\ H3 by Th57; :: thesis: verum

H1 /\ H3 is Subgroup of H2 /\ H3

let H1, H2, H3 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 implies H1 /\ H3 is Subgroup of H2 /\ H3 )

assume H1 is Subgroup of H2 ; :: thesis: H1 /\ H3 is Subgroup of H2 /\ H3

then the carrier of H1 c= the carrier of H2 by Def5;

then the carrier of H1 /\ the carrier of H3 c= the carrier of H2 /\ the carrier of H3 by XBOOLE_1:26;

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

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

hence H1 /\ H3 is Subgroup of H2 /\ H3 by Th57; :: thesis: verum