set f = the Equivalence_Relation of M;

defpred S_{1}[ object ] means $1 is Equivalence_Relation of M;

deffunc H_{1}( 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_{1}(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_{1}[x] ) )
from XBOOLE_0:sch 1();

A3: for EqR being Equivalence_Relation of M holds EqR in product M2

then reconsider B = B as non empty set by A2;

defpred S_{2}[ 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_{2}[x,y,z]

A9: for x, y being Element of B holds S_{2}[x,y,B1 . (x,y)]
from BINOP_1:sch 3(A6);

defpred S_{3}[ 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_{3}[x,y,z]

A13: for x, y being Element of B holds S_{3}[x,y,B2 . (x,y)]
from BINOP_1:sch 3(A10);

reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;

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

defpred S

deffunc H

consider M2 being ManySortedSet of I such that

A1: for i being Element of I holds M2 . i = H

consider B being set such that

A2: for x being object holds

( x in B iff ( x in product M2 & S

A3: for EqR being Equivalence_Relation of M holds EqR in product M2

proof

then
the Equivalence_Relation of M in product M2
;
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

.= dom M2 by PARTFUN1:def 2 ;

hence EqR in product M2 by A4, CARD_3:9; :: thesis: verum

end;A4: for x being object st x in dom M2 holds

EqR . x in M2 . x

proof

dom EqR =
I
by PARTFUN1:def 2
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;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

.= dom M2 by PARTFUN1:def 2 ;

hence EqR in product M2 by A4, CARD_3:9; :: thesis: verum

then reconsider B = B as non empty set by A2;

defpred S

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

proof

consider B1 being BinOp of B such that
let x, y be Element of B; :: thesis: ex z being Element of B st S_{2}[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_{2}[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;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

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

A9: for x, y being Element of B holds S

defpred S

$3 = x1 (/\) y1;

A10: for x, y being Element of B ex z being Element of B st S

proof

consider B2 being BinOp of B such that
let x, y be Element of B; :: thesis: ex z being Element of B st S_{3}[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)

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)

z in product M2 by A3;

then reconsider z = z as Element of B by A2;

take z ; :: thesis: S_{3}[x,y,z]

thus S_{3}[x,y,z]
; :: thesis: verum

end;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

then reconsider z = x9 (/\) y9 as ManySortedRelation of M by MSUALG_4:def 1;
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;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

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

then reconsider z = z as Equivalence_Relation of M by MSUALG_4:def 2;
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 A12, PBOOLE:def 5;

hence R is Equivalence_Relation of (M . i) ; :: thesis: verum

end;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

z in product M2 by A3;

then reconsider z = z as Element of B by A2;

take z ; :: thesis: S

thus S

A13: for x, y being Element of B holds S

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;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

A16: now :: thesis: for a, b, c being Element of B holds B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)

A17:
for a, b, c being Element of L holds a "\/" (b "\/" c) = (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;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

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;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

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;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

A22: now :: thesis: for a, b, c being Element of B holds B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)

A23:
for a, b, c being Element of L holds a "/\" (b "/\" c) = (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;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

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;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

A25: now :: thesis: for a, b being Element of B holds B1 . (a,b) = B1 . (b,a)

A26:
for a, b being Element of L holds a "\/" b = 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;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

proof

A27:
for a, b being Element of L holds (a "/\" b) "\/" b = b
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;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

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

.= b by A28, LATTICES:def 2 ; :: thesis: verum

end;reconsider x = a, y = b as Element of B ;

A28: B1 . ((B2 . (x,y)),y) = y

proof

thus (a "/\" b) "\/" b =
the L_join of L . ((a "/\" b),b)
by LATTICES:def 1
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;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

.= b by A28, LATTICES:def 2 ; :: thesis: verum

A29: now :: thesis: for a, b being Element of B holds B2 . (a,b) = B2 . (b,a)

A30:
for a, b being Element of L holds a "/\" b = 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;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

proof

for a, b being Element of L holds a "/\" (a "\/" b) = a
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;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

proof

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;
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

.= a by A31, LATTICES:def 1 ; :: thesis: verum

end;reconsider x = a, y = b as Element of B ;

A31: B2 . (x,(B1 . (x,y))) = x

proof

thus a "/\" (a "\/" b) =
the L_meet of L . (a,(a "\/" b))
by LATTICES:def 2
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;B1 . (x,y) = U1 "\/" U2 by A14;

hence B2 . (x,(B1 . (x,y))) = U1 (/\) (U1 "\/" U2) by A19

.= x by Th9 ;

:: thesis: verum

.= a by A31, LATTICES:def 1 ; :: thesis: verum

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