set f = the Equivalence_Relation of M;
defpred S1[ object ] means $1 is Equivalence_Relation of M;
deffunc H1( Element of I) -> set = bool [:(M . $1),(M . $1):];
consider M2 being ManySortedSet of I such that
A1:
for i being Element of I holds M2 . i = H1(i)
from PBOOLE:sch 5();
consider B being set such that
A2:
for x being object holds
( x in B iff ( x in product M2 & S1[x] ) )
from XBOOLE_0:sch 1();
A3:
for EqR being Equivalence_Relation of M holds EqR in product M2
then
the Equivalence_Relation of M in product M2
;
then reconsider B = B as non empty set by A2;
defpred S2[ Element of B, Element of B, Element of B] means for x1, y1 being Equivalence_Relation of M st x1 = $1 & y1 = $2 holds
ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 (\/) y1 & $3 = EqCl EqR3 );
A6:
for x, y being Element of B ex z being Element of B st S2[x,y,z]
consider B1 being BinOp of B such that
A9:
for x, y being Element of B holds S2[x,y,B1 . (x,y)]
from BINOP_1:sch 3(A6);
defpred S3[ Element of B, Element of B, Element of B] means for x1, y1 being Equivalence_Relation of M st x1 = $1 & y1 = $2 holds
$3 = x1 (/\) y1;
A10:
for x, y being Element of B ex z being Element of B st S3[x,y,z]
consider B2 being BinOp of B such that
A13:
for x, y being Element of B holds S3[x,y,B2 . (x,y)]
from BINOP_1:sch 3(A10);
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A16:
now for a, b, c being Element of B holds B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)let a,
b,
c be
Element of
B;
B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)reconsider U1 =
a,
U2 =
b,
U3 =
c as
Equivalence_Relation of
M by A2;
thus B1 . (
a,
(B1 . (b,c))) =
B1 . (
a,
(U2 "\/" U3))
by A14
.=
U1 "\/" (U2 "\/" U3)
by A14
.=
(U1 "\/" U2) "\/" U3
by Th8
.=
B1 . (
(U1 "\/" U2),
c)
by A14
.=
B1 . (
(B1 . (a,b)),
c)
by A14
;
verum end;
A17:
for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a,
b,
c be
Element of
L;
a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider x =
a,
y =
b,
z =
c as
Element of
B ;
A18:
the
L_join of
L . (
a,
b)
= a "\/" b
by LATTICES:def 1;
thus a "\/" (b "\/" c) =
the
L_join of
L . (
a,
(b "\/" c))
by LATTICES:def 1
.=
B1 . (
x,
(B1 . (y,z)))
by LATTICES:def 1
.=
the
L_join of
L . (
( the L_join of L . (a,b)),
c)
by A16
.=
(a "\/" b) "\/" c
by A18, LATTICES:def 1
;
verum
end;
A22:
now for a, b, c being Element of B holds B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)let a,
b,
c be
Element of
B;
B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)reconsider U1 =
a,
U2 =
b,
U3 =
c as
Equivalence_Relation of
M by A2;
reconsider EQR1 =
U2 (/\) U3 as
Equivalence_Relation of
M by Th11;
reconsider EQR2 =
U1 (/\) U2 as
Equivalence_Relation of
M by Th11;
thus B2 . (
a,
(B2 . (b,c))) =
B2 . (
a,
EQR1)
by A19
.=
U1 (/\) (U2 (/\) U3)
by A19
.=
(U1 (/\) U2) (/\) U3
by PBOOLE:29
.=
B2 . (
EQR2,
c)
by A19
.=
B2 . (
(B2 . (a,b)),
c)
by A19
;
verum end;
A23:
for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a,
b,
c be
Element of
L;
a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider x =
a,
y =
b,
z =
c as
Element of
B ;
A24:
the
L_meet of
L . (
a,
b)
= a "/\" b
by LATTICES:def 2;
thus a "/\" (b "/\" c) =
the
L_meet of
L . (
a,
(b "/\" c))
by LATTICES:def 2
.=
B2 . (
x,
(B2 . (y,z)))
by LATTICES:def 2
.=
the
L_meet of
L . (
( the L_meet of L . (a,b)),
c)
by A22
.=
(a "/\" b) "/\" c
by A24, LATTICES:def 2
;
verum
end;
A25:
now for a, b being Element of B holds B1 . (a,b) = B1 . (b,a)end;
A26:
for a, b being Element of L holds a "\/" b = b "\/" a
A27:
for a, b being Element of L holds (a "/\" b) "\/" b = b
A29:
now for a, b being Element of B holds B2 . (a,b) = B2 . (b,a)end;
A30:
for a, b being Element of L holds a "/\" b = b "/\" a
for a, b being Element of L holds a "/\" (a "\/" b) = a
then
( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
by A26, A17, A27, A30, A23, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
then reconsider L = L as strict Lattice ;
take
L
; ( ( for x being set holds
( x in the carrier of L iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of L . (x,y) = x (/\) y & the L_join of L . (x,y) = x "\/" y ) ) )
thus
for x being set holds
( x in the carrier of L iff x is Equivalence_Relation of M )
by A2, A3; for x, y being Equivalence_Relation of M holds
( the L_meet of L . (x,y) = x (/\) y & the L_join of L . (x,y) = x "\/" y )
thus
for x, y being Equivalence_Relation of M holds
( the L_meet of L . (x,y) = x (/\) y & the L_join of L . (x,y) = x "\/" y )
by A14, A19; verum