for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting