let G be addGroup; :: 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 /\ the carrier of H3 c= the carrier of H2 /\ the carrier of H3 by DefA5, 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