:: deftheorem defines kernel_congruence WAYBEL20:def 4 :
for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k = [:k,k:] " (id the carrier of L);