let G be Group; :: thesis: for H1, H2, H3 being Subgroup of G st H1 is Subgroup of H2 & H1 is Subgroup of H3 holds
H1 is Subgroup of H2 /\ H3
let H1, H2, H3 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 & H1 is Subgroup of H3 implies H1 is Subgroup of H2 /\ H3 )
assume A1: ( H1 is Subgroup of H2 & H1 is Subgroup of H3 ) ; :: thesis: H1 is Subgroup of H2 /\ H3

now

let g be Element of G; :: thesis: ( g in H1 implies g in H2 /\ H3 )
assume g in H1 ; :: thesis: g in H2 /\ H3
then ( g in H2 & g in H3 ) by A1, Th49;
hence g in H2 /\ H3 by Th99; :: thesis: verum

end;

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