let X be Subset of (EqRelLATT A); :: according to LATTICE5:def 2 :: thesis:
set B = X /\ the carrier of (EqRelLATT A);
X /\ the carrier of (EqRelLATT A) c= bool [:A,A:]

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X /\ the carrier of (EqRelLATT A) ; :: thesis:
then x is Equivalence_Relation of A by Th4;
hence x in bool [:A,A:] ; :: thesis:

end;

then reconsider B = X /\ the carrier of (EqRelLATT A) as Subset-Family of [:A,A:] ;
consider b being Subset of [:A,A:] such that
A1: b = Intersect B ;
for x being object st x in A holds
[x,x] in b

let x be object ; :: thesis:
assume A2: x in A ; :: thesis:
A3: for Y being set st Y in B holds
[x,x] in Y

let Y be set ; :: thesis:
assume Y in B ; :: thesis:
then Y is Equivalence_Relation of A by Th4;
hence [x,x] in Y by A2, EQREL_1:5; :: thesis:

end;

[x,x] in [:A,A:] by A2, ZFMISC_1:def 2;
hence [x,x] in b by A1, A3, SETFAM_1:43; :: thesis:

end;

then A4: b is_reflexive_in A by RELAT_2:def 1;
reconsider b = b as Relation of A ;
A5: ( dom b = A & field b = A ) by A4, ORDERS_1:13;
for x, y, z being object st x in A & y in A & z in A & [x,y] in b & [y,z] in b holds
[x,z] in b

let x, y, z be object ; :: thesis:
assume that
A6: x in A and
y in A and
A7: z in A and
A8: ( [x,y] in b & [y,z] in b ) ; :: thesis:
A9: for Y being set st Y in B holds
[x,z] in Y

let Y be set ; :: thesis:
assume A10: Y in B ; :: thesis:
then A11: Y is Equivalence_Relation of A by Th4;
( [x,y] in Y & [y,z] in Y ) by A1, A8, A10, SETFAM_1:43;
hence [x,z] in Y by A11, EQREL_1:7; :: thesis:

end;

[x,z] in [:A,A:] by A6, A7, ZFMISC_1:def 2;
hence [x,z] in b by A1, A9, SETFAM_1:43; :: thesis:

end;

then A12: b is_transitive_in A by RELAT_2:def 8;
for x, y being object st x in A & y in A & [x,y] in b holds
[y,x] in b

let x, y be object ; :: thesis:
assume that
A13: ( x in A & y in A ) and
A14: [x,y] in b ; :: thesis:
A15: for Y being set st Y in B holds
[y,x] in Y

let Y be set ; :: thesis:
assume Y in B ; :: thesis:
then ( [x,y] in Y & Y is Equivalence_Relation of A ) by A1, A14, Th4, SETFAM_1:43;
hence [y,x] in Y by EQREL_1:6; :: thesis:

end;

[y,x] in [:A,A:] by A13, ZFMISC_1:def 2;
hence [y,x] in b by A1, A15, SETFAM_1:43; :: thesis:

end;

then b is_symmetric_in A by RELAT_2:def 3;
then reconsider b = b as Equivalence_Relation of A by A5, A12, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
reconsider b = b as Element of (EqRelLATT A) by Th4;
take b ; :: thesis:

let a be Element of (EqRelLATT A); :: thesis:
reconsider a9 = a as Equivalence_Relation of A by Th4;
reconsider b9 = b as Equivalence_Relation of A ;
assume a in X /\ the carrier of (EqRelLATT A) ; :: thesis:
then for x, y being object st [x,y] in b9 holds
[x,y] in a9 by A1, SETFAM_1:43;
then b9 c= a9 by RELAT_1:def 3;
hence b <= a by Th6; :: thesis:

end;

then b is_<=_than X /\ the carrier of (EqRelLATT A) ;
hence b is_<=_than X by YELLOW_0:5; :: thesis:
let a be Element of (EqRelLATT A); :: thesis:
reconsider a9 = a as Equivalence_Relation of A by Th4;
assume a is_<=_than X ; :: thesis:
then A16: a is_<=_than X /\ the carrier of (EqRelLATT A) by YELLOW_0:5;
A17: for d being Element of (EqRelLATT A) st d in B holds
a9 c= d by A16, Th6;
a9 c= Intersect B

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: x in a9 ; :: thesis:
for Y being set st Y in B holds
x in Y

let Y be set ; :: thesis:
assume Y in B ; :: thesis:
then a9 c= Y by A17;
hence x in Y by A18; :: thesis:

end;

hence x in Intersect B by A18, SETFAM_1:43; :: thesis:

end;

hence a <= b by A1, Th6; :: thesis: