theorem :: WAYBEL20:42

for L being complete continuous LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
R = kernel_congruence (kernel_op R) by Th36;