:: deftheorem Def3 defines kernel_op WAYBEL20:def 3 :
for L being complete LATTICE
for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for b₃ being kernel Function of L,L holds
( b₃ = kernel_op R iff for x being Element of L holds b₃ . x = inf (Class ((EqRel R),x)) );