let G be addGroup; :: 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 :: thesis: for g being Element of G st g in H1 holds
g 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;
hence H1 is Subgroup of H2 /\ H3 by Th58; :: thesis: verum