let L be complete LATTICE; :: thesis: for R being non empty Subset of [:L,L:] st R is CLCongruence holds
for x being Element of L holds [(inf (Class (EqRel R),x)),x] in R
let R be non empty Subset of [:L,L:]; :: thesis: ( R is CLCongruence implies for x being Element of L holds [(inf (Class (EqRel R),x)),x] in R )
assume A1: R is CLCongruence ; :: thesis: for x being Element of L holds [(inf (Class (EqRel R),x)),x] in R
let x be Element of L; :: thesis: [(inf (Class (EqRel R),x)),x] in R
set CRx = Class (EqRel R),x;
reconsider SR = [:(Class (EqRel R),x),{x}:] as Subset of [:L,L:] ;
R is Equivalence_Relation of the carrier of L by A1, Def2;
then A2: R = EqRel R by Def1;
SR c= the carrier of (subrelstr R)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in SR or a in the carrier of (subrelstr R) )
assume a in SR ; :: thesis: a in the carrier of (subrelstr R)
then consider a1, a2 being set such that
A3: a1 in Class (EqRel R),x and
A4: a2 in {x} and
A5: a = [a1,a2] by ZFMISC_1:def 2;
a2 = x by A4, TARSKI:def 1;
then a in R by A2, A3, A5, EQREL_1:27;
hence a in the carrier of (subrelstr R) by YELLOW_0:def 15; :: thesis: verum

end;

then reconsider SR9 = SR as Subset of (subrelstr R) ;
A6: ex_inf_of SR,[:L,L:] by YELLOW_0:17;
subrelstr R is CLSubFrame of [:L,L:] by A1, Def2;
then A7: "/\" SR9,[:L,L:] in the carrier of (subrelstr R) by A6, YELLOW_0:def 18;
A8: x in Class (EqRel R),x by EQREL_1:28;
inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17
.= [(inf (Class (EqRel R),x)),(inf (proj2 SR))] by FUNCT_5:11
.= [(inf (Class (EqRel R),x)),(inf {x})] by A8, FUNCT_5:11
.= [(inf (Class (EqRel R),x)),x] by YELLOW_0:39 ;
hence [(inf (Class (EqRel R),x)),x] in R by A7, YELLOW_0:def 15; :: thesis: verum