set f = the Equivalence_Relation of M;
defpred S₁[ object ] means $1 is Equivalence_Relation of M;
deffunc H₁( 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 = H₁(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 & S₁[x] ) ) from XBOOLE_0:sch 1();
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 A4, CARD_3:9; :: thesis: verum

end;

then the Equivalence_Relation of M in product M2 ;
then reconsider B = B as non empty set by A2;
defpred S₂[ 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 S₂[x,y,z]

proof

let x, y be Element of B; :: thesis: ex z being Element of B st S₂[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: S₂[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 S₂[x,y,B1 . (x,y)] from BINOP_1:sch 3(A6);
defpred S₃[ 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 S₃[x,y,z]

proof

let x, y be Element of B; :: thesis: ex z being Element of B st S₃[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 object
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 object ; :: 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 A12, PBOOLE:def 5;
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: S₃[x,y,z]
thus S₃[x,y,z] ; :: thesis: verum

end;

consider B2 being BinOp of B such that
A13: for x, y being Element of B holds S₃[x,y,B2 . (x,y)] from BINOP_1:sch 3(A10);
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 A2, A15;
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 A18, LATTICES:def 1 ; :: 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 A2, A20;
A21: y9 = y ;
x9 = x ;
hence B2 . (x,y) = x (/\) y by A13, A21; :: 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 A24, LATTICES:def 2 ; :: 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 A28, LATTICES:def 2 ; :: 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 A31, LATTICES:def 1 ; :: 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 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 ; :: 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 A14, A19; :: thesis: verum