for L being complete continuous LATTICE
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L & ex LR being complete continuous LATTICE st
( the carrier of LR = Class (EqRel R) & ( for g being Function of L,LR st ( for x being Element of L holds g . x = Class ((EqRel R),x) ) holds
g is CLHomomorphism of L,LR ) ) holds
subrelstr R is CLSubFrame of [:L,L:]