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:]
ex LR being strict complete continuous LATTICE st
( the carrier of LR = Class (EqRel (kernel_congruence k)) & 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 } & ( 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 Th37;
hence subrelstr (kernel_congruence k) is CLSubFrame of [:L,L:] by A1, Th38; :: thesis: verum