defpred S₁[ Element of L, Element of (EqRelLATT A)] means ex E being Equivalence_Relation of A st
( E = $2 & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= $1 ) ) );
A1: for e being Element of L ex r being Element of (EqRelLATT A) st S₁[e,r]

proof

let e be Element of L; :: thesis: ex r being Element of (EqRelLATT A) st S₁[e,r]
defpred S₂[ Element of A, Element of A] means d . $1,$2 <= e;
consider E being Relation of A,A such that
A2: for x, y being Element of A holds
( [x,y] in E iff S₂[x,y] ) from RELSET_1:sch 2();
for x being set st x in A holds
[x,x] in E

proof

let x be set ; :: thesis: ( x in A implies [x,x] in E )
assume x in A ; :: thesis: [x,x] in E
then reconsider x' = x as Element of A ;
Bottom L <= e by YELLOW_0:44;
then d . x',x' <= e by Def7;
hence [x,x] in E by A2; :: thesis: verum

end;

then E is_reflexive_in A by RELAT_2:def 1;
then A3: ( dom E = A & field E = A ) by ORDERS_1:98;
for x, y being set st x in A & y in A & [x,y] in E holds
[y,x] in E

proof

let x, y be set ; :: thesis: ( x in A & y in A & [x,y] in E implies [y,x] in E )
assume that
A4: ( x in A & y in A ) and
A5: [x,y] in E ; :: thesis: [y,x] in E
reconsider x' = x as Element of A by A4;
reconsider y' = y as Element of A by A4;
d . x',y' <= e by A2, A5;
then d . y',x' <= e by Def6;
hence [y,x] in E by A2; :: thesis: verum

end;

then A6: E is_symmetric_in A by RELAT_2:def 3;
for x, y, z being set st x in A & y in A & z in A & [x,y] in E & [y,z] in E holds
[x,z] in E

proof

let x, y, z be set ; :: thesis: ( x in A & y in A & z in A & [x,y] in E & [y,z] in E implies [x,z] in E )
assume that
A7: ( x in A & y in A & z in A ) and
A8: ( [x,y] in E & [y,z] in E ) ; :: thesis: [x,z] in E
reconsider x' = x, y' = y, z' = z as Element of A by A7;
( d . x',y' <= e & d . y',z' <= e ) by A2, A8;
then A9: (d . x',y') "\/" (d . y',z') <= e by YELLOW_0:22;
d . x',z' <= (d . x',y') "\/" (d . y',z') by Def8;
then d . x',z' <= e by A9, ORDERS_2:26;
hence [x,z] in E by A2; :: thesis: verum

end;

then E is_transitive_in A by RELAT_2:def 8;
then reconsider E = E as Equivalence_Relation of A by A3, A6, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
reconsider E = E as Element of (EqRelLATT A) by Th4;
consider r being Element of (EqRelLATT A) such that
A10: r = E ;
thus ex r being Element of (EqRelLATT A) st S₁[e,r] by A2, A10; :: thesis: verum

end;

consider f being Function of L,(EqRelLATT A) such that
A11: for e being Element of L holds S₁[e,f . e] from FUNCT_2:sch 10(A1);
thus ex b₁ being Function of L,(EqRelLATT A) st
for e being Element of L ex E being Equivalence_Relation of A st
( E = b₁ . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) ) by A11; :: thesis: verum