A2: R is Equivalence_Relation of the carrier of L by A1, Def2;
A3: subrelstr R is CLSubFrame of [:L,L:] by A1, Def2;
deffunc H₁( Element of L) -> Element of the carrier of L = inf (Class (EqRel R),$1);
consider k being Function of the carrier of L,the carrier of L such that
A4: for x being Element of L holds k . x = H₁(x) from FUNCT_2:sch 4();
A5: R = EqRel R by A2, Def1;
reconsider k = k as Function of L,L ;
A6: k is projection

proof

now

let x be Element of L; :: thesis: (k * k) . x = k . x
set CRx = Class (EqRel R),x;
A7: k . x = inf (Class (EqRel R),x) by A4;
then A8: k . (k . x) = inf (Class (EqRel R),(inf (Class (EqRel R),x))) by A4;
[(inf (Class (EqRel R),x)),x] in R by A1, Th36;
then inf (Class (EqRel R),x) in Class (EqRel R),x by A5, EQREL_1:27;
then Class (EqRel R),(inf (Class (EqRel R),x)) = Class (EqRel R),x by EQREL_1:31;
hence (k * k) . x = k . x by A7, A8, FUNCT_2:21; :: thesis: verum

end;

then k * k = k by FUNCT_2:113;
hence k is idempotent by QUANTAL1:def 9; :: according to WAYBEL_1:def 13 :: thesis: k is monotone
thus k is monotone :: thesis: verum

proof

let x, y be Element of L; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or k . x <= k . y )
assume A9: x <= y ; :: thesis: k . x <= k . y
A10: inf {x,y} = x "/\" y by YELLOW_0:40
.= x by A9, YELLOW_0:25 ;
set CRx = Class (EqRel R),x;
set CRy = Class (EqRel R),y;
reconsider SR = {[(inf (Class (EqRel R),x)),x],[(inf (Class (EqRel R),y)),y]} as Subset of [:L,L:] ;
( [(inf (Class (EqRel R),x)),x] in R & [(inf (Class (EqRel R),y)),y] in R ) by A1, Th36;
then SR c= R by ZFMISC_1:38;
then reconsider SR' = SR as Subset of (subrelstr R) by YELLOW_0:def 15;
A11: ex_inf_of SR,[:L,L:] by YELLOW_0:17;
then A12: inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7
.= [(inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))}),(inf (proj2 SR))] by FUNCT_5:16
.= [(inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))}),(inf {x,y})] by FUNCT_5:16 ;
"/\" SR',[:L,L:] in the carrier of (subrelstr R) by A3, A11, YELLOW_0:def 18;
then [(inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))}),x] in R by A10, A12, YELLOW_0:def 15;
then inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))} in Class (EqRel R),x by A5, EQREL_1:27;
then A13: inf (Class (EqRel R),x) <= inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))} by YELLOW_2:24;
inf (Class (EqRel R),y) in {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))} by TARSKI:def 2;
then A14: inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))} <= inf (Class (EqRel R),y) by YELLOW_2:24;
( k . x = inf (Class (EqRel R),x) & k . y = inf (Class (EqRel R),y) ) by A4;
hence k . x <= k . y by A13, A14, YELLOW_0:def 2; :: thesis: verum

end;

end;

now

let x be Element of L; :: thesis: k . x <= (id L) . x
A15: k . x = inf (Class (EqRel R),x) by A4;
set CRx = Class (EqRel R),x;
A16: x in Class (EqRel R),x by EQREL_1:28;
inf (Class (EqRel R),x) is_<=_than Class (EqRel R),x by YELLOW_0:33;
then inf (Class (EqRel R),x) <= x by A16, LATTICE3:def 8;
hence k . x <= (id L) . x by A15, FUNCT_1:35; :: thesis: verum

end;

then k <= id L by YELLOW_2:10;
then reconsider k = k as kernel Function of L,L by A6, WAYBEL_1:def 15;
take k ; :: thesis: for x being Element of L holds k . x = inf (Class (EqRel R),x)
thus for x being Element of L holds k . x = inf (Class (EqRel R),x) by A4; :: thesis: verum