let L be complete continuous LATTICE; :: thesis: for k being directed-sups-preserving kernel Function of L,L holds kernel_congruence k is CLCongruence
let k be directed-sups-preserving kernel Function of L,L; :: thesis: kernel_congruence k is CLCongruence
set R = kernel_congruence k;
thus A1: kernel_congruence k is Equivalence_Relation of the carrier of L by Th2; :: according to WAYBEL20:def 2 :: thesis: subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:]
consider LR being strict complete continuous LATTICE such that
A2: the carrier of LR = Class (EqRel (kernel_congruence k)) and
the InternalRel of LR = { [(Class (EqRel (kernel_congruence k)),x),(Class (EqRel (kernel_congruence k)),y)] where x, y is Element of L : k . x <= k . y } and
A3: for g being Function of L,LR st ( for x being Element of L holds g . x = Class (EqRel (kernel_congruence k)),x ) holds
g is CLHomomorphism of L,LR by Th38;
thus subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:] by A1, A2, A3, Th39; :: thesis: verum