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;
then A3: R = EqRel R by Def1;
A4: subrelstr R is CLSubFrame of [:L,L:] by A1;
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:13
.= [(inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))}),(inf {x,y})] by FUNCT_5:13 ;
( [(inf (Class ((EqRel R),x))),x] in R & [(inf (Class ((EqRel R),y))),y] in R ) by A1, Th35;
then SR c= R by ZFMISC_1:32;
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:19;
then A9: inf (Class ((EqRel R),x)) <= inf {(inf (Class ((EqRel R),x))),(inf (Class ((EqRel R),y)))} by YELLOW_2:22;
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:22;
( 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 :: thesis: for x being Element of L holds (k * k) . x = k . x

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, Th35;
then inf (Class ((EqRel R),x)) in Class ((EqRel R),x) by A3, EQREL_1:19;
then A11: Class ((EqRel R),(inf (Class ((EqRel R),x)))) = Class ((EqRel R),x) by EQREL_1:23;
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:15; :: thesis: verum

end;

then k * k = k by FUNCT_2:63;
then k is idempotent by QUANTAL1:def 9;
then A13: k is projection by A5;

now :: thesis: for x being Element of L holds k . x <= (id L) . x

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:20, YELLOW_0:33;
then A14: inf (Class ((EqRel R),x)) <= x ;
k . x = inf (Class ((EqRel R),x)) by A2;
hence k . x <= (id L) . x by A14, FUNCT_1:18; :: thesis: verum

end;

then k <= id L by YELLOW_2:9;
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