let X be Subset of (EqRelLATT A); :: according to LATTICE5:def 2 :: thesis: ex a being Element of (EqRelLATT A) st
( a is_<=_than X & ( for b being Element of (EqRelLATT A) st b is_<=_than X holds
b <= a ) )
set B = X /\ the carrier of (EqRelLATT A);
X /\ the carrier of (EqRelLATT A) c= bool [:A,A:]

proof

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

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

proof

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

proof

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

end;

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

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

proof

let x, y, z be object ; :: thesis: ( x in A & y in A & z in A & [x,y] in b & [y,z] in b implies [x,z] in b )
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: [x,z] in b
A9: for Y being set st Y in B holds
[x,z] in Y

proof

let Y be set ; :: thesis: ( Y in B implies [x,z] in Y )
assume A10: Y in B ; :: thesis: [x,z] in Y
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: verum

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: verum

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

proof

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

proof

let Y be set ; :: thesis: ( Y in B implies [y,x] in Y )
assume Y in B ; :: thesis: [y,x] in Y
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: verum

end;

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

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: ( b is_<=_than X & ( for b being Element of (EqRelLATT A) st b is_<=_than X holds
b <= b ) )

now :: thesis: for a being Element of (EqRelLATT A) st a in X /\ the carrier of (EqRelLATT A) holds
b <= a

let a be Element of (EqRelLATT A); :: thesis: ( a in X /\ the carrier of (EqRelLATT A) implies b <= a )
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: b <= a
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: verum

end;

then b is_<=_than X /\ the carrier of (EqRelLATT A) ;
hence b is_<=_than X by YELLOW_0:5; :: thesis: for b being Element of (EqRelLATT A) st b is_<=_than X holds
b <= b
let a be Element of (EqRelLATT A); :: thesis: ( a is_<=_than X implies a <= b )
reconsider a9 = a as Equivalence_Relation of A by Th4;
assume a is_<=_than X ; :: thesis: a <= b
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

proof

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

proof

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

end;

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

end;

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