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;
then A2: R = EqRel R by Def1;
SR c= the carrier of (subrelstr R)
proof
let a be object ; :: 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 object 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:19;
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;
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:20;
inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17
.= [(inf (Class ((EqRel R),x))),(inf (proj2 SR))] by FUNCT_5:9
.= [(inf (Class ((EqRel R),x))),(inf {x})] by A8, FUNCT_5:9
.= [(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