for G1, G2 being Group
for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is Homomorphism of (lattice G1),(lattice G2) by Th31, Th32;