for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )