set D = the carrier of (EqRelLatt the Sorts of A);

set f = the MSCongruence of A;

defpred S_{1}[ object ] means $1 is MSCongruence of A;

deffunc H_{1}( Element of S) -> set = bool [:( the Sorts of A . $1),( the Sorts of A . $1):];

consider M2 being ManySortedSet of the carrier of S such that

A1: for i being Element of the carrier of S 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 C1 being MSCongruence of A holds C1 in product M2

( x in B iff x is MSCongruence of A ) by A2, A3;

then the MSCongruence of A in B ;

then reconsider B = B as non empty set ;

set B1 = the L_join of (EqRelLatt the Sorts of A) || B;

set B2 = the L_meet of (EqRelLatt the Sorts of A) || B;

then [:B,B:] c= [: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):] by ZFMISC_1:96;

then reconsider B1 = the L_join of (EqRelLatt the Sorts of A) || B, B2 = the L_meet of (EqRelLatt the Sorts of A) || B as Function of [:B,B:], the carrier of (EqRelLatt the Sorts of A) by FUNCT_2:32;

A8: dom B2 = [:B,B:] by FUNCT_2:def 1;

A13: dom B1 = [:B,B:] by FUNCT_2:def 1;

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

A18: for a, b being MSCongruence of A holds

( B1 . (a,b) = a "\/" b & B2 . (a,b) = a (/\) b )

then reconsider L = L as Lattice ;

reconsider L = L as strict SubLattice of EqRelLatt the Sorts of A by A7, NAT_LAT:def 12;

take L ; :: thesis: for x being set holds

( x in the carrier of L iff x is MSCongruence of A )

thus for x being set holds

( x in the carrier of L iff x is MSCongruence of A ) by A6; :: thesis: verum

set f = the MSCongruence of A;

defpred S

deffunc H

consider M2 being ManySortedSet of the carrier of S such that

A1: for i being Element of the carrier of S 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 C1 being MSCongruence of A holds C1 in product M2

proof

A6:
for x being set holds
let C1 be MSCongruence of A; :: thesis: C1 in product M2

.= dom M2 by PARTFUN1:def 2 ;

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

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

C1 . x in M2 . x

dom C1 =
the carrier of S
by PARTFUN1:def 2
C1 . x in M2 . x

let x be object ; :: thesis: ( x in dom M2 implies C1 . x in M2 . x )

assume x in dom M2 ; :: thesis: C1 . x in M2 . x

then reconsider x9 = x as Element of the carrier of S ;

A5: C1 . x9 is Subset of [:( the Sorts of A . x9),( the Sorts of A . x9):] ;

M2 . x9 = bool [:( the Sorts of A . x9),( the Sorts of A . x9):] by A1;

hence C1 . x in M2 . x by A5; :: thesis: verum

end;assume x in dom M2 ; :: thesis: C1 . x in M2 . x

then reconsider x9 = x as Element of the carrier of S ;

A5: C1 . x9 is Subset of [:( the Sorts of A . x9),( the Sorts of A . x9):] ;

M2 . x9 = bool [:( the Sorts of A . x9),( the Sorts of A . x9):] by A1;

hence C1 . x in M2 . x by A5; :: thesis: verum

.= dom M2 by PARTFUN1:def 2 ;

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

( x in B iff x is MSCongruence of A ) by A2, A3;

then the MSCongruence of A in B ;

then reconsider B = B as non empty set ;

set B1 = the L_join of (EqRelLatt the Sorts of A) || B;

set B2 = the L_meet of (EqRelLatt the Sorts of A) || B;

now :: thesis: for x being object st x in B holds

x in the carrier of (EqRelLatt the Sorts of A)

then A7:
B c= the carrier of (EqRelLatt the Sorts of A)
by TARSKI:def 3;x in the carrier of (EqRelLatt the Sorts of A)

let x be object ; :: thesis: ( x in B implies x in the carrier of (EqRelLatt the Sorts of A) )

assume x in B ; :: thesis: x in the carrier of (EqRelLatt the Sorts of A)

then x is MSCongruence of A by A6;

hence x in the carrier of (EqRelLatt the Sorts of A) by Def5; :: thesis: verum

end;assume x in B ; :: thesis: x in the carrier of (EqRelLatt the Sorts of A)

then x is MSCongruence of A by A6;

hence x in the carrier of (EqRelLatt the Sorts of A) by Def5; :: thesis: verum

then [:B,B:] c= [: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):] by ZFMISC_1:96;

then reconsider B1 = the L_join of (EqRelLatt the Sorts of A) || B, B2 = the L_meet of (EqRelLatt the Sorts of A) || B as Function of [:B,B:], the carrier of (EqRelLatt the Sorts of A) by FUNCT_2:32;

A8: dom B2 = [:B,B:] by FUNCT_2:def 1;

now :: thesis: for x being object st x in [:B,B:] holds

B2 . x in B

then reconsider B2 = B2 as BinOp of B by A8, FUNCT_2:3;B2 . x in B

let x be object ; :: thesis: ( x in [:B,B:] implies B2 . x in B )

assume A9: x in [:B,B:] ; :: thesis: B2 . x in B

then consider x1, x2 being object such that

A10: x = [x1,x2] by RELAT_1:def 1;

A11: x2 in B by A9, A10, ZFMISC_1:87;

x1 in B by A9, A10, ZFMISC_1:87;

then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A11;

A12: x29 in B by A6;

x19 in B by A6;

then [x1,x2] in [:B,B:] by A12, ZFMISC_1:87;

then B2 . x = the L_meet of (EqRelLatt the Sorts of A) . (x1,x2) by A10, FUNCT_1:49

.= x19 (/\) x29 by Def5 ;

then B2 . x is MSCongruence of A by Th16;

hence B2 . x in B by A6; :: thesis: verum

end;assume A9: x in [:B,B:] ; :: thesis: B2 . x in B

then consider x1, x2 being object such that

A10: x = [x1,x2] by RELAT_1:def 1;

A11: x2 in B by A9, A10, ZFMISC_1:87;

x1 in B by A9, A10, ZFMISC_1:87;

then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A11;

A12: x29 in B by A6;

x19 in B by A6;

then [x1,x2] in [:B,B:] by A12, ZFMISC_1:87;

then B2 . x = the L_meet of (EqRelLatt the Sorts of A) . (x1,x2) by A10, FUNCT_1:49

.= x19 (/\) x29 by Def5 ;

then B2 . x is MSCongruence of A by Th16;

hence B2 . x in B by A6; :: thesis: verum

A13: dom B1 = [:B,B:] by FUNCT_2:def 1;

now :: thesis: for x being object st x in [:B,B:] holds

B1 . x in B

then reconsider B1 = B1 as BinOp of B by A13, FUNCT_2:3;B1 . x in B

let x be object ; :: thesis: ( x in [:B,B:] implies B1 . x in B )

assume A14: x in [:B,B:] ; :: thesis: B1 . x in B

then consider x1, x2 being object such that

A15: x = [x1,x2] by RELAT_1:def 1;

A16: x2 in B by A14, A15, ZFMISC_1:87;

x1 in B by A14, A15, ZFMISC_1:87;

then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A16;

A17: x29 in B by A6;

x19 in B by A6;

then [x1,x2] in [:B,B:] by A17, ZFMISC_1:87;

then B1 . x = the L_join of (EqRelLatt the Sorts of A) . (x1,x2) by A15, FUNCT_1:49

.= x19 "\/" x29 by Def5 ;

then B1 . x is MSCongruence of A by Th15;

hence B1 . x in B by A6; :: thesis: verum

end;assume A14: x in [:B,B:] ; :: thesis: B1 . x in B

then consider x1, x2 being object such that

A15: x = [x1,x2] by RELAT_1:def 1;

A16: x2 in B by A14, A15, ZFMISC_1:87;

x1 in B by A14, A15, ZFMISC_1:87;

then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A16;

A17: x29 in B by A6;

x19 in B by A6;

then [x1,x2] in [:B,B:] by A17, ZFMISC_1:87;

then B1 . x = the L_join of (EqRelLatt the Sorts of A) . (x1,x2) by A15, FUNCT_1:49

.= x19 "\/" x29 by Def5 ;

then B1 . x is MSCongruence of A by Th15;

hence B1 . x in B by A6; :: thesis: verum

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

A18: for a, b being MSCongruence of A holds

( B1 . (a,b) = a "\/" b & B2 . (a,b) = a (/\) b )

proof

let a, b be MSCongruence of A; :: thesis: ( B1 . (a,b) = a "\/" b & B2 . (a,b) = a (/\) b )

A19: b in B by A6;

a in B by A6;

then A20: [a,b] in [:B,B:] by A19, ZFMISC_1:87;

hence B1 . (a,b) = the L_join of (EqRelLatt the Sorts of A) . (a,b) by FUNCT_1:49

.= a "\/" b by Def5 ;

:: thesis: B2 . (a,b) = a (/\) b

thus B2 . (a,b) = the L_meet of (EqRelLatt the Sorts of A) . (a,b) by A20, FUNCT_1:49

.= a (/\) b by Def5 ; :: thesis: verum

end;A19: b in B by A6;

a in B by A6;

then A20: [a,b] in [:B,B:] by A19, ZFMISC_1:87;

hence B1 . (a,b) = the L_join of (EqRelLatt the Sorts of A) . (a,b) by FUNCT_1:49

.= a "\/" b by Def5 ;

:: thesis: B2 . (a,b) = a (/\) b

thus B2 . (a,b) = the L_meet of (EqRelLatt the Sorts of A) . (a,b) by A20, FUNCT_1:49

.= a (/\) b by Def5 ; :: thesis: verum

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

A22:
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 a9 = a, b9 = b as MSCongruence of A by A6;

thus B1 . (a,b) = a9 "\/" b9 by A18

.= B1 . (b,a) by A18 ; :: thesis: verum

end;reconsider a9 = a, b9 = b as MSCongruence of A by A6;

thus B1 . (a,b) = a9 "\/" b9 by A18

.= B1 . (b,a) by A18 ; :: thesis: verum

proof

let a, b be Element of L; :: thesis: a "\/" b = b "\/" a

thus a "\/" b = B1 . (a,b) by LATTICES:def 1

.= the L_join of L . (b,a) by A21

.= b "\/" a by LATTICES:def 1 ; :: thesis: verum

end;thus a "\/" b = B1 . (a,b) by LATTICES:def 1

.= the L_join of L . (b,a) by A21

.= b "\/" a by LATTICES:def 1 ; :: thesis: verum

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

A24:
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 a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;

reconsider e1 = b9 (/\) c9 as MSCongruence of A by Th16;

reconsider e2 = a9 (/\) b9 as MSCongruence of A by Th16;

thus B2 . (a,(B2 . (b,c))) = B2 . (a,e1) by A18

.= a9 (/\) (b9 (/\) c9) by A18

.= (a9 (/\) b9) (/\) c9 by PBOOLE:29

.= B2 . (e2,c) by A18

.= B2 . ((B2 . (a,b)),c) by A18 ; :: thesis: verum

end;reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;

reconsider e1 = b9 (/\) c9 as MSCongruence of A by Th16;

reconsider e2 = a9 (/\) b9 as MSCongruence of A by Th16;

thus B2 . (a,(B2 . (b,c))) = B2 . (a,e1) by A18

.= a9 (/\) (b9 (/\) c9) by A18

.= (a9 (/\) b9) (/\) c9 by PBOOLE:29

.= B2 . (e2,c) by A18

.= B2 . ((B2 . (a,b)),c) by A18 ; :: thesis: verum

proof

let a, b, c be Element of L; :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c

thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def 2

.= B2 . (a,(B2 . (b,c))) by LATTICES:def 2

.= the L_meet of L . (( the L_meet of L . (a,b)),c) by A23

.= the L_meet of L . ((a "/\" b),c) by LATTICES:def 2

.= (a "/\" b) "/\" c by LATTICES:def 2 ; :: thesis: verum

end;thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by LATTICES:def 2

.= B2 . (a,(B2 . (b,c))) by LATTICES:def 2

.= the L_meet of L . (( the L_meet of L . (a,b)),c) by A23

.= the L_meet of L . ((a "/\" b),c) by LATTICES:def 2

.= (a "/\" b) "/\" c by LATTICES:def 2 ; :: thesis: verum

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

A26:
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 a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;

reconsider d = b9 "\/" c9 as MSCongruence of A by Th15;

reconsider e = a9 "\/" b9 as MSCongruence of A by Th15;

thus B1 . (a,(B1 . (b,c))) = B1 . (a,d) by A18

.= a9 "\/" (b9 "\/" c9) by A18

.= (a9 "\/" b9) "\/" c9 by Th8

.= B1 . (e,c) by A18

.= B1 . ((B1 . (a,b)),c) by A18 ; :: thesis: verum

end;reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;

reconsider d = b9 "\/" c9 as MSCongruence of A by Th15;

reconsider e = a9 "\/" b9 as MSCongruence of A by Th15;

thus B1 . (a,(B1 . (b,c))) = B1 . (a,d) by A18

.= a9 "\/" (b9 "\/" c9) by A18

.= (a9 "\/" b9) "\/" c9 by Th8

.= B1 . (e,c) by A18

.= B1 . ((B1 . (a,b)),c) by A18 ; :: thesis: verum

proof

let a, b, c be Element of L; :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c

thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def 1

.= B1 . (a,(B1 . (b,c))) by LATTICES:def 1

.= the L_join of L . (( the L_join of L . (a,b)),c) by A25

.= the L_join of L . ((a "\/" b),c) by LATTICES:def 1

.= (a "\/" b) "\/" c by LATTICES:def 1 ; :: thesis: verum

end;thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by LATTICES:def 1

.= B1 . (a,(B1 . (b,c))) by LATTICES:def 1

.= the L_join of L . (( the L_join of L . (a,b)),c) by A25

.= the L_join of L . ((a "\/" b),c) by LATTICES:def 1

.= (a "\/" b) "\/" c by LATTICES:def 1 ; :: thesis: verum

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

A28:
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 a9 = a, b9 = b as MSCongruence of A by A6;

thus B2 . (a,b) = b9 (/\) a9 by A18

.= B2 . (b,a) by A18 ; :: thesis: verum

end;reconsider a9 = a, b9 = b as MSCongruence of A by A6;

thus B2 . (a,b) = b9 (/\) a9 by A18

.= B2 . (b,a) by A18 ; :: thesis: verum

proof

A29:
for a, b being Element of L holds a "/\" (a "\/" b) = a
let a, b be Element of L; :: thesis: a "/\" b = b "/\" a

thus a "/\" b = B2 . (a,b) by LATTICES:def 2

.= the L_meet of L . (b,a) by A27

.= b "/\" a by LATTICES:def 2 ; :: thesis: verum

end;thus a "/\" b = B2 . (a,b) by LATTICES:def 2

.= the L_meet of L . (b,a) by A27

.= b "/\" a by LATTICES:def 2 ; :: thesis: verum

proof

for a, b being Element of L holds (a "/\" b) "\/" b = b
let a, b be Element of L; :: thesis: a "/\" (a "\/" b) = a

A30: B2 . (a,(B1 . (a,b))) = a

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

end;A30: B2 . (a,(B1 . (a,b))) = a

proof

thus a "/\" (a "\/" b) =
the L_meet of L . (a,(a "\/" b))
by LATTICES:def 2
reconsider a9 = a, b9 = b as MSCongruence of A by A6;

reconsider d = a9 "\/" b9 as MSCongruence of A by Th15;

thus B2 . (a,(B1 . (a,b))) = B2 . (a,d) by A18

.= a9 (/\) (a9 "\/" b9) by A18

.= a by Th9 ; :: thesis: verum

end;reconsider d = a9 "\/" b9 as MSCongruence of A by Th15;

thus B2 . (a,(B1 . (a,b))) = B2 . (a,d) by A18

.= a9 (/\) (a9 "\/" b9) by A18

.= a by Th9 ; :: thesis: verum

.= a by A30, LATTICES:def 1 ; :: 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 A22, A26, A28, A24, A29, 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 "/\" b) "\/" b = b

A31: B1 . ((B2 . (a,b)),b) = b

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

end;A31: B1 . ((B2 . (a,b)),b) = b

proof

thus (a "/\" b) "\/" b =
the L_join of L . ((a "/\" b),b)
by LATTICES:def 1
reconsider a9 = a, b9 = b as MSCongruence of A by A6;

reconsider EQR = a9 (/\) b9 as MSCongruence of A by Th16;

thus B1 . ((B2 . (a,b)),b) = B1 . ((a9 (/\) b9),b9) by A18

.= EQR "\/" b9 by A18

.= b by Th10 ; :: thesis: verum

end;reconsider EQR = a9 (/\) b9 as MSCongruence of A by Th16;

thus B1 . ((B2 . (a,b)),b) = B1 . ((a9 (/\) b9),b9) by A18

.= EQR "\/" b9 by A18

.= b by Th10 ; :: thesis: verum

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

then reconsider L = L as Lattice ;

reconsider L = L as strict SubLattice of EqRelLatt the Sorts of A by A7, NAT_LAT:def 12;

take L ; :: thesis: for x being set holds

( x in the carrier of L iff x is MSCongruence of A )

thus for x being set holds

( x in the carrier of L iff x is MSCongruence of A ) by A6; :: thesis: verum