set D = the carrier of (EqRelLatt the Sorts of A);
set f = the MSCongruence of A;
defpred S₁[ object ] means $1 is MSCongruence of A;
deffunc H₁( 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₁(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 C1 being MSCongruence of A holds C1 in product M2

proof

let C1 be MSCongruence of A; :: thesis: C1 in product M2

A4: now :: thesis: for x being object st x in dom M2 holds
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;

dom C1 = the carrier of S by PARTFUN1:def 2
.= dom M2 by PARTFUN1:def 2 ;
hence C1 in product M2 by A4, CARD_3:9; :: thesis: verum

end;

A6: for x being set holds
( 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)

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;

then A7: B c= the carrier of (EqRelLatt the Sorts of A) by TARSKI:def 3;
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

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;

then reconsider B2 = B2 as BinOp of B by A8, FUNCT_2:3;
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

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;

then reconsider B1 = B1 as BinOp of B by A13, FUNCT_2:3;
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;

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

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

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

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

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

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

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

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

A29: 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
A30: B2 . (a,(B1 . (a,b))) = a

proof

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;

thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by LATTICES:def 2
.= a by A30, LATTICES:def 1 ; :: thesis: verum

end;

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
A31: B1 . ((B2 . (a,b)),b) = b

proof

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;

thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by LATTICES:def 1
.= b by A31, LATTICES:def 2 ; :: 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 A22, A26, A28, A24, A29, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
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