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 A3: for EqR being Equivalence_Relation of M holds EqR in product M2
proof
let EqR be Equivalence_Relation of M; :: thesis: EqR in product M2
A4: for x being object st x in dom M2 holds
EqR . x in M2 . x
proof
let x be object ; :: thesis: ( x in dom M2 implies EqR . x in M2 . x )
assume x in dom M2 ; :: thesis: EqR . x in M2 . x
then reconsider x9 = x as Element of I ;
A5: EqR . x9 is Subset of [:(M . x9),(M . x9):] ;
M2 . x9 = bool [:(M . x9),(M . x9):] by A1;
hence EqR . x in M2 . x by A5; :: thesis: verum
end;
dom EqR = I by PARTFUN1:def 2
.= dom M2 by PARTFUN1:def 2 ;
hence EqR in product M2 by ; :: thesis: verum
end;
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]
proof
let x, y be Element of B; :: thesis: ex z being Element of B st S2[x,y,z]
reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;
set z = x9 "\/" y9;
x9 "\/" y9 in product M2 by A3;
then reconsider z = x9 "\/" y9 as Element of B by A2;
take z ; :: thesis: S2[x,y,z]
let x1, y1 be Equivalence_Relation of M; :: thesis: ( x1 = x & y1 = y implies ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 (\/) y1 & z = EqCl EqR3 ) )

assume that
A7: x1 = x and
A8: y1 = y ; :: thesis: ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 (\/) y1 & z = EqCl EqR3 )

thus ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 (\/) y1 & z = EqCl EqR3 ) by A7, A8, Def4; :: thesis: verum
end;
consider B1 being BinOp of B such that
A9: for x, y being Element of B holds S2[x,y,B1 . (x,y)] from 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]
proof
let x, y be Element of B; :: thesis: ex z being Element of B st S3[x,y,z]
reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;
set z = x9 (/\) y9;
for i being set st i in I holds
(x9 (/\) y9) . i is Relation of (M . i)
proof
let i be set ; :: thesis: ( i in I implies (x9 (/\) y9) . i is Relation of (M . i) )
assume i in I ; :: thesis: (x9 (/\) y9) . i is Relation of (M . i)
then reconsider i9 = i as Element of I ;
(x9 (/\) y9) . i = (x9 . i9) /\ (y9 . i9) by PBOOLE:def 5;
hence (x9 (/\) y9) . i is Relation of (M . i) ; :: thesis: verum
end;
then reconsider z = x9 (/\) y9 as ManySortedRelation of M by MSUALG_4:def 1;
for i being set
for R being Relation of (M . i) st i in I & z . i = R holds
R is Equivalence_Relation of (M . i)
proof
let i be set ; :: thesis: for R being Relation of (M . i) st i in I & z . i = R holds
R is Equivalence_Relation of (M . i)

let R be Relation of (M . i); :: thesis: ( i in I & z . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A11: i in I and
A12: z . i = R ; :: thesis: R is Equivalence_Relation of (M . i)
reconsider i9 = i as Element of I by A11;
reconsider x199 = x9 . i9, y199 = y9 . i9 as Relation of (M . i) ;
reconsider x99 = x199, y99 = y199 as Equivalence_Relation of (M . i) by MSUALG_4:def 2;
R = x99 /\ y99 by ;
hence R is Equivalence_Relation of (M . i) ; :: thesis: verum
end;
then reconsider z = z as Equivalence_Relation of M by MSUALG_4:def 2;
z in product M2 by A3;
then reconsider z = z as Element of B by A2;
take z ; :: thesis: S3[x,y,z]
thus S3[x,y,z] ; :: thesis: verum
end;
consider B2 being BinOp of B such that
A13: for x, y being Element of B holds S3[x,y,B2 . (x,y)] from reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A14: now :: thesis: for x, y being Equivalence_Relation of M holds B1 . (x,y) = x "\/" y
let x, y be Equivalence_Relation of M; :: thesis: B1 . (x,y) = x "\/" y
A15: y in product M2 by A3;
x in product M2 by A3;
then reconsider x9 = x, y9 = y as Element of B by ;
ex EqR3 being ManySortedRelation of M st
( EqR3 = x (\/) y & B1 . (x9,y9) = EqCl EqR3 ) by A9;
hence B1 . (x,y) = x "\/" y by Def4; :: thesis: verum
end;
A16: now :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum
end;
A19: now :: thesis: for x, y being Equivalence_Relation of M holds B2 . (x,y) = x (/\) y
let x, y be Equivalence_Relation of M; :: thesis: B2 . (x,y) = x (/\) y
A20: y in product M2 by A3;
x in product M2 by A3;
then reconsider x9 = x, y9 = y as Element of B by ;
A21: y9 = y ;
x9 = x ;
hence B2 . (x,y) = x (/\) y by ; :: thesis: verum
end;
A22: now :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum
end;
A25: now :: thesis: for a, b being Element of B holds B1 . (a,b) = B1 . (b,a)
let a, b be Element of B; :: thesis: B1 . (a,b) = B1 . (b,a)
reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;
thus B1 . (a,b) = U1 "\/" U2 by A14
.= B1 . (b,a) by A14 ; :: thesis: verum
end;
A26: for a, b being Element of L holds a "\/" b = b "\/" a
proof
let a, b be Element of L; :: thesis: a "\/" b = b "\/" a
reconsider x = a, y = b as Element of B ;
thus a "\/" b = B1 . (x,y) by LATTICES:def 1
.= the L_join of L . (b,a) by A25
.= b "\/" a by LATTICES:def 1 ; :: thesis: verum
end;
A27: for a, b being Element of L holds (a "/\" b) "\/" b = b
proof
let a, b be Element of L; :: thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of B ;
A28: B1 . ((B2 . (x,y)),y) = y
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
reconsider EQR = U1 (/\) U2 as Equivalence_Relation of M by Th11;
B2 . (x,y) = U1 (/\) U2 by A19;
hence B1 . ((B2 . (x,y)),y) = EQR "\/" U2 by A14
.= y by Th10 ;
:: thesis: verum
end;
thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def 1
.= b by ; :: thesis: verum
end;
A29: now :: thesis: for a, b being Element of B holds B2 . (a,b) = B2 . (b,a)
let a, b be Element of B; :: thesis: B2 . (a,b) = B2 . (b,a)
reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;
thus B2 . (a,b) = U2 (/\) U1 by A19
.= B2 . (b,a) by A19 ; :: thesis: verum
end;
A30: for a, b being Element of L holds a "/\" b = b "/\" a
proof
let a, b be Element of L; :: thesis: a "/\" b = b "/\" a
reconsider x = a, y = b as Element of B ;
thus a "/\" b = B2 . (x,y) by LATTICES:def 2
.= the L_meet of L . (b,a) by A29
.= b "/\" a by LATTICES:def 2 ; :: thesis: verum
end;
for a, b being Element of L holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L; :: thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of B ;
A31: B2 . (x,(B1 . (x,y))) = x
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
B1 . (x,y) = U1 "\/" U2 by A14;
hence B2 . (x,(B1 . (x,y))) = U1 (/\) (U1 "\/" U2) by A19
.= x by Th9 ;
:: thesis: verum
end;
thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def 2
.= a by ; :: thesis: verum
end;
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 ;
then reconsider L = L as strict Lattice ;
take L ; :: thesis: ( ( 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; :: thesis: 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 ; :: thesis: verum