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

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

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

H1 /\ H3 is Subgroup of H1 by Lm4;

hence H1 /\ H3 is Subgroup of H2 by A1, Th56; :: thesis: verum

H1 /\ H3 is Subgroup of H2

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

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

H1 /\ H3 is Subgroup of H1 by Lm4;

hence H1 /\ H3 is Subgroup of H2 by A1, Th56; :: thesis: verum