for L being lower-bounded LATTICE
for x, y being Element of L
for A being non empty set
for f being Homomorphism of L,(EqRelLATT A) st f is V17() & (corestr f) . x <= (corestr f) . y holds
x <= y