theorem :: WAYBEL20:39

for L being non empty reflexive RelStr
for k being kernel Function of L,L holds kernel_congruence k is Equivalence_Relation of the carrier of L by Th2;