let X be Subset of (EqRelLATT A); LATTICE5:def 2 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:]
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
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 ;
( 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 )
;
[x,z] in b
A9:
for
Y being
set st
Y in B holds
[x,z] in Y
[x,z] in [:A,A:]
by A6, A7, ZFMISC_1:def 2;
hence
[x,z] in b
by A1, A9, SETFAM_1:43;
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 ;
( 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
;
[y,x] in b
A15:
for
Y being
set st
Y in B holds
[y,x] in Y
[y,x] in [:A,A:]
by A13, ZFMISC_1:def 2;
hence
[y,x] in b
by A1, A15, SETFAM_1:43;
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
; ( b is_<=_than X & ( for b being Element of (EqRelLATT A) st b is_<=_than X holds
b <= b ) )
then
b is_<=_than X /\ the carrier of (EqRelLATT A)
;
hence
b is_<=_than X
by YELLOW_0:5; for b being Element of (EqRelLATT A) st b is_<=_than X holds
b <= b
let a be Element of (EqRelLATT A); ( a is_<=_than X implies a <= b )
reconsider a9 = a as Equivalence_Relation of A by Th4;
assume
a is_<=_than X
; 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
hence
a <= b
by A1, Th6; verum