let G1, G2 be Group; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( not H1 is Subgroup of H2 or H3 is Subgroup of H4 )
assume H1 is Subgroup of H2 ; :: thesis: 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:66, RELAT_1:178; :: thesis: verum