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
then A2: R is Equivalence_Relation of the carrier of L by Def2;
A3: subrelstr R is CLSubFrame of [:L,L:] by A1, Def2;
A4: R = EqRel R by A2, Def1;
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:] ;
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
A5: ( a1 in Class (EqRel R),x & a2 in {x} & a = [a1,a2] ) by ZFMISC_1:def 2;
a2 = x by A5, TARSKI:def 1;
then a in R by A4, A5, EQREL_1:27;
hence a in the carrier of (subrelstr R) by YELLOW_0:def 15; :: thesis: verum

end;

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