theorem :: LATTICE5:44

for L being lower-bounded LATTICE ex A being non empty set ex f being Homomorphism of L,(EqRelLATT A) st
( f is one-to-one & type_of (Image f) <= 3 )