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

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 :: thesis: for g being Element of G st g in H1 holds

g in H2 /\ H3

hence
H1 is Subgroup of H2 /\ H3
by Th58; :: thesis: verumg in H2 /\ H3

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, Th40;

hence g in H2 /\ H3 by Th82; :: thesis: verum

end;assume g in H1 ; :: thesis: g in H2 /\ H3

then ( g in H2 & g in H3 ) by A1, Th40;

hence g in H2 /\ H3 by Th82; :: thesis: verum