let G1, G2 be Group; for f being Homomorphism of G1,G2
for H1, H2 being Subgroup of G2
for H3, H4 being Subgroup of G1 st the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 holds
H3 is Subgroup of H4
let f be Homomorphism of G1,G2; for H1, H2 being Subgroup of G2
for H3, H4 being Subgroup of G1 st the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 holds
H3 is Subgroup of H4
let H1, H2 be Subgroup of G2; for H3, H4 being Subgroup of G1 st the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 holds
H3 is Subgroup of H4
let H3, H4 be Subgroup of G1; ( the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 & H1 is Subgroup of H2 implies H3 is Subgroup of H4 )
assume A1:
( the carrier of H3 = f " the carrier of H1 & the carrier of H4 = f " the carrier of H2 )
; ( not H1 is Subgroup of H2 or H3 is Subgroup of H4 )
assume
H1 is Subgroup of H2
; H3 is Subgroup of H4
then
the carrier of H1 c= the carrier of H2
by GROUP_2:def 5;
hence
H3 is Subgroup of H4
by A1, GROUP_2:57, RELAT_1:143; verum