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
A2: for x being Element of L holds k . x = H₁(x) from FUNCT_2:sch 4();
reconsider k = k as Function of L,L ;
R is Equivalence_Relation of the carrier of L by A1, Def2;
then A3: R = EqRel R by Def1;
A4: subrelstr R is CLSubFrame of [:L,L:] by A1, Def2;
A5: k is monotone

proof

let x, y be Element of L; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or k . x <= k . y )
assume A6: x <= y ; :: thesis: k . x <= k . y
set CRy = Class (EqRel R),y;
set CRx = Class (EqRel R),x;
reconsider SR = {[(inf (Class (EqRel R),x)),x],[(inf (Class (EqRel R),y)),y]} as Subset of [:L,L:] ;
A7: inf SR = [(inf (proj1 SR)),(inf (proj2 SR))] by Th7, YELLOW_0:17
.= [(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 ;
( [(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 SR9 = SR as Subset of (subrelstr R) by YELLOW_0:def 15;
ex_inf_of SR,[:L,L:] by YELLOW_0:17;
then A8: "/\" SR9,[:L,L:] in the carrier of (subrelstr R) by A4, YELLOW_0:def 18;
inf {x,y} = x "/\" y by YELLOW_0:40
.= x by A6, YELLOW_0:25 ;
then [(inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))}),x] in R by A7, A8, YELLOW_0:def 15;
then inf {(inf (Class (EqRel R),x)),(inf (Class (EqRel R),y))} in Class (EqRel R),x by A3, EQREL_1:27;
then A9: 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 A10: 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 A2;
hence k . x <= k . y by A9, A10, YELLOW_0:def 2; :: thesis: verum

end;

now

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

end;

then k * k = k by FUNCT_2:113;
then k is idempotent by QUANTAL1:def 9;
then A13: k is projection by A5, WAYBEL_1:def 13;

now

let x be Element of L; :: thesis: k . x <= (id L) . x
set CRx = Class (EqRel R),x;
( x in Class (EqRel R),x & inf (Class (EqRel R),x) is_<=_than Class (EqRel R),x ) by EQREL_1:28, YELLOW_0:33;
then A14: inf (Class (EqRel R),x) <= x by LATTICE3:def 8;
k . x = inf (Class (EqRel R),x) by A2;
hence k . x <= (id L) . x by A14, 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 A13, 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 A2; :: thesis: verum