let L be complete LATTICE; :: thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
let R be non empty Subset of [:L,L:]; :: thesis: ( R is CLCongruence implies ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) )
assume A1: R is CLCongruence ; :: thesis: ( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
then A2: R is Equivalence_Relation of the carrier of L by Def2;
then A3: EqRel R = R by Def1;
A4: subrelstr R is CLSubFrame of [:L,L:] by A1, Def2;
set k = kernel_op R;
set cL = the carrier of L;
A5: dom (kernel_op R) = the carrier of L by FUNCT_2:def 1;
thus kernel_op R is directed-sups-preserving :: thesis: R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L)

proof

let D be Subset of L; :: according to WAYBEL_0:def 37 :: thesis: ( D is empty or not D is directed or kernel_op R preserves_sup_of D )
assume that
A6: ( not D is empty & D is directed ) and
ex_sup_of D,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (kernel_op R) .: D,L & "\/" ((kernel_op R) .: D),L = (kernel_op R) . ("\/" D,L) )
thus ex_sup_of (kernel_op R) .: D,L by YELLOW_0:17; :: thesis: "\/" ((kernel_op R) .: D),L = (kernel_op R) . ("\/" D,L)
set d = sup D;
set ds = sup ((kernel_op R) .: D);
(kernel_op R) .: D is_<=_than (kernel_op R) . (sup D)

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in (kernel_op R) .: D or b <= (kernel_op R) . (sup D) )
assume b in (kernel_op R) .: D ; :: thesis: b <= (kernel_op R) . (sup D)
then consider a being set such that
A7: ( a in dom (kernel_op R) & a in D & b = (kernel_op R) . a ) by FUNCT_1:def 12;
reconsider a = a as Element of L by A7;
D is_<=_than sup D by YELLOW_0:32;
then a <= sup D by A7, LATTICE3:def 9;
hence b <= (kernel_op R) . (sup D) by A7, WAYBEL_1:def 2; :: thesis: verum

end;

then A8: sup ((kernel_op R) .: D) <= (kernel_op R) . (sup D) by YELLOW_0:32;
set S = { [((kernel_op R) . x),x] where x is Element of L : x in D } ;
A9: the carrier of (subrelstr R) = R by YELLOW_0:def 15;
A10: { [((kernel_op R) . x),x] where x is Element of L : x in D } c= R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [((kernel_op R) . x),x] where x is Element of L : x in D } or x in R )
assume x in { [((kernel_op R) . x),x] where x is Element of L : x in D } ; :: thesis: x in R
then consider a being Element of L such that
A11: ( x = [((kernel_op R) . a),a] & a in D ) ;
(kernel_op R) . a = inf (Class (EqRel R),a) by A1, Def3;
hence x in R by A1, A11, Th36; :: thesis: verum

end;

then reconsider S' = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of (subrelstr R) by YELLOW_0:def 15;
reconsider S = { [((kernel_op R) . x),x] where x is Element of L : x in D } as Subset of [:L,L:] by A10, XBOOLE_1:1;
A12: ex_sup_of S,[:L,L:] by YELLOW_0:17;
consider e being set such that
A13: e in D by A6, XBOOLE_0:def 1;
reconsider e = e as Element of L by A13;
A14: [((kernel_op R) . e),e] in S by A13;
A15: S' is directed

proof

let x, y be Element of (subrelstr R); :: according to WAYBEL_0:def 1 :: thesis: ( not x in S' or not y in S' or ex b₁ being Element of the carrier of (subrelstr R) st
( b₁ in S' & x <= b₁ & y <= b₁ ) )
assume A16: ( x in S' & y in S' ) ; :: thesis: ex b₁ being Element of the carrier of (subrelstr R) st
( b₁ in S' & x <= b₁ & y <= b₁ )
then consider a being Element of L such that
A17: ( x = [((kernel_op R) . a),a] & a in D ) ;
consider b being Element of L such that
A18: ( y = [((kernel_op R) . b),b] & b in D ) by A16;
consider c being Element of L such that
A19: ( c in D & a <= c & b <= c ) by A6, A17, A18, WAYBEL_0:def 1;
set z = [((kernel_op R) . c),c];
[((kernel_op R) . c),c] in S' by A19;
then reconsider z = [((kernel_op R) . c),c] as Element of (subrelstr R) ;
take z ; :: thesis: ( z in S' & x <= z & y <= z )
thus z in S' by A19; :: thesis: ( x <= z & y <= z )
(kernel_op R) . a <= (kernel_op R) . c by A19, WAYBEL_1:def 2;
then [((kernel_op R) . a),a] <= [((kernel_op R) . c),c] by A19, YELLOW_3:11;
hence x <= z by A17, YELLOW_0:61; :: thesis: y <= z
(kernel_op R) . b <= (kernel_op R) . c by A19, WAYBEL_1:def 2;
then [((kernel_op R) . b),b] <= [((kernel_op R) . c),c] by A19, YELLOW_3:11;
hence y <= z by A18, YELLOW_0:61; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( x in proj1 S implies x in (kernel_op R) .: D ) & ( x in (kernel_op R) .: D implies x in proj1 S ) )

hereby :: thesis: ( x in (kernel_op R) .: D implies x in proj1 S )

assume x in proj1 S ; :: thesis: x in (kernel_op R) .: D
then consider y being set such that
A20: [x,y] in S by RELAT_1:def 4;
consider a being Element of L such that
A21: ( [x,y] = [((kernel_op R) . a),a] & a in D ) by A20;
x = (kernel_op R) . a by A21, ZFMISC_1:33;
hence x in (kernel_op R) .: D by A5, A21, FUNCT_1:def 12; :: thesis: verum

end;

assume x in (kernel_op R) .: D ; :: thesis: x in proj1 S
then consider y being set such that
A22: ( y in dom (kernel_op R) & y in D & x = (kernel_op R) . y ) by FUNCT_1:def 12;
reconsider y = y as Element of L by A22;
[((kernel_op R) . y),y] in S by A22;
hence x in proj1 S by A22, RELAT_1:def 4; :: thesis: verum

end;

then A23: proj1 S = (kernel_op R) .: D by TARSKI:2;

now

let x be set ; :: thesis: ( ( x in proj2 S implies x in D ) & ( x in D implies x in proj2 S ) )

hereby :: thesis: ( x in D implies x in proj2 S )

assume x in proj2 S ; :: thesis: x in D
then consider y being set such that
A24: [y,x] in S by RELAT_1:def 5;
consider a being Element of L such that
A25: ( [y,x] = [((kernel_op R) . a),a] & a in D ) by A24;
thus x in D by A25, ZFMISC_1:33; :: thesis: verum

end;

assume A26: x in D ; :: thesis: x in proj2 S
then reconsider x' = x as Element of L ;
[((kernel_op R) . x'),x'] in S by A26;
hence x in proj2 S by RELAT_1:def 5; :: thesis: verum

end;

then proj2 S = D by TARSKI:2;
then sup S = [(sup ((kernel_op R) .: D)),(sup D)] by A12, A23, Th8;
then [(sup ((kernel_op R) .: D)),(sup D)] in R by A4, A9, A12, A14, A15, WAYBEL_0:def 4;
then A27: sup ((kernel_op R) .: D) in Class (EqRel R),(sup D) by A3, EQREL_1:27;
(kernel_op R) . (sup D) = inf (Class (EqRel R),(sup D)) by A1, Def3;
then (kernel_op R) . (sup D) <= sup ((kernel_op R) .: D) by A27, YELLOW_2:24;
hence "\/" ((kernel_op R) .: D),L = (kernel_op R) . ("\/" D,L) by A8, YELLOW_0:def 3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( x in R implies x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ) & ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R ) )

hereby :: thesis: ( x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) implies x in R )

assume A28: x in R ; :: thesis: x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L)
then x in the carrier of [:L,L:] ;
then x in [:the carrier of L,the carrier of L:] by YELLOW_3:def 2;
then consider x1, x2 being set such that
A29: ( x1 in the carrier of L & x2 in the carrier of L & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of L by A29;
A30: ( (kernel_op R) . x1 = inf (Class (EqRel R),x1) & (kernel_op R) . x2 = inf (Class (EqRel R),x2) ) by A1, Def3;
x1 in Class (EqRel R),x2 by A3, A28, A29, EQREL_1:27;
then (kernel_op R) . x1 = (kernel_op R) . x2 by A30, EQREL_1:31;
then A31: [((kernel_op R) . x1),((kernel_op R) . x2)] in id the carrier of L by RELAT_1:def 10;
A32: [:(kernel_op R),(kernel_op R):] . x1,x2 = [((kernel_op R) . x1),((kernel_op R) . x2)] by A5, FUNCT_3:def 9;
dom [:(kernel_op R),(kernel_op R):] = [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def 9;
then [x1,x2] in dom [:(kernel_op R),(kernel_op R):] by A5, ZFMISC_1:106;
hence x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by A29, A31, A32, FUNCT_1:def 13; :: thesis: verum

end;

assume x in [:(kernel_op R),(kernel_op R):] " (id the carrier of L) ; :: thesis: x in R
then A33: ( x in dom [:(kernel_op R),(kernel_op R):] & [:(kernel_op R),(kernel_op R):] . x in id the carrier of L ) by FUNCT_1:def 13;
then x in [:(dom (kernel_op R)),(dom (kernel_op R)):] by FUNCT_3:def 9;
then consider x1, x2 being set such that
A34: ( x1 in dom (kernel_op R) & x2 in dom (kernel_op R) & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of L by A34;
[:(kernel_op R),(kernel_op R):] . x1,x2 = [((kernel_op R) . x1),((kernel_op R) . x2)] by A34, FUNCT_3:def 9;
then A35: (kernel_op R) . x1 = (kernel_op R) . x2 by A33, A34, RELAT_1:def 10;
( (kernel_op R) . x1 = inf (Class (EqRel R),x1) & (kernel_op R) . x2 = inf (Class (EqRel R),x2) ) by A1, Def3;
then A36: ( [((kernel_op R) . x1),x1] in R & [((kernel_op R) . x2),x2] in R ) by A1, Th36;
then [x1,((kernel_op R) . x1)] in R by A2, EQREL_1:12;
hence x in R by A2, A34, A35, A36, EQREL_1:13; :: thesis: verum

end;

hence R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) by TARSKI:2; :: thesis: verum