theorem :: WAYBEL20:43
for L being complete continuous LATTICE
for k being directed-sups-preserving kernel Function of L,L holds k = kernel_op (kernel_congruence k)