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, y being object st x in A & y in A & [x,y] in E holds
[y,x] in E

proof

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

end;

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

proof

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

end;

then E is_reflexive_in A by RELAT_2:def 1;
then A7: ( dom E = A & field E = A ) by ORDERS_1:13;
for x, y, z being object 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 object ; :: 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
A8: ( x in A & y in A & z in A ) and
A9: ( [x,y] in E & [y,z] in E ) ; :: thesis: [x,z] in E
reconsider x9 = x, y9 = y, z9 = z as Element of A by A8;
( d . (x9,y9) <= e & d . (y9,z9) <= e ) by A2, A9;
then A10: (d . (x9,y9)) "\/" (d . (y9,z9)) <= e by YELLOW_0:22;
d . (x9,z9) <= (d . (x9,y9)) "\/" (d . (y9,z9)) by Def7;
then d . (x9,z9) <= e by A10, ORDERS_2:3;
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 A7, A6, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
reconsider E = E as Element of (EqRelLATT A) by Th4;
ex r being Element of (EqRelLATT A) st r = E ;
hence ex r being Element of (EqRelLATT A) st S₁[e,r] by A2; :: thesis: verum

end;

ex f being Function of L,(EqRelLATT A) st
for e being Element of L holds S₁[e,f . e] from FUNCT_2:sch 3(A1);
hence 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 ) ) ) ; :: thesis: verum