for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being Element of L holds [(inf (Class ((EqRel R),x))),x] in R