set D = the carrier of (EqRelLatt the Sorts of A);
consider f being MSCongruence of A;
defpred S₁[ set ] 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 set 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

let C1 be MSCongruence of A; :: thesis:

A4: now

let x be set ; :: thesis:
assume x in dom M2 ; :: thesis:
then reconsider x9 = x as Element of the carrier of S by PARTFUN1:def 4;
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:

end;

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

end;

A6: for x being set holds
( x in B iff x is MSCongruence of A )

proof

let x be set ; :: thesis:
thus ( x in B implies x is MSCongruence of A ) by A2; :: thesis:
thus ( x is MSCongruence of A implies x in B ) :: thesis:

proof

assume A7: x is MSCongruence of A ; :: thesis:
then x in product M2 by A3;
hence x in B by A2, A7; :: thesis:

end;

then f 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

let x be set ; :: thesis:
assume x in B ; :: thesis:
then x is MSCongruence of A by A6;
hence x in the carrier of (EqRelLatt the Sorts of A) by Def5; :: thesis:

end;

then A8: 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:119;
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:38;
A9: dom B2 = [:B,B:] by FUNCT_2:def 1;

now

let x be set ; :: thesis:
assume A10: x in [:B,B:] ; :: thesis:
then consider x1, x2 being set such that
A11: x = [x1,x2] by RELAT_1:def 1;
A12: x2 in B by A10, A11, ZFMISC_1:106;
x1 in B by A10, A11, ZFMISC_1:106;
then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A12;
A13: x29 in B by A6;
x19 in B by A6;
then [x1,x2] in [:B,B:] by A13, ZFMISC_1:106;
then B2 . x = the L_meet of (EqRelLatt the Sorts of A) . x1,x2 by A11, FUNCT_1:72
.= x19 /\ x29 by Def5 ;
then B2 . x is MSCongruence of A by Th18;
hence B2 . x in B by A6; :: thesis:

end;

then reconsider B2 = B2 as BinOp of B by A9, FUNCT_2:5;
A14: dom B1 = [:B,B:] by FUNCT_2:def 1;

now

let x be set ; :: thesis:
assume A15: x in [:B,B:] ; :: thesis:
then consider x1, x2 being set such that
A16: x = [x1,x2] by RELAT_1:def 1;
A17: x2 in B by A15, A16, ZFMISC_1:106;
x1 in B by A15, A16, ZFMISC_1:106;
then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6, A17;
A18: x29 in B by A6;
x19 in B by A6;
then [x1,x2] in [:B,B:] by A18, ZFMISC_1:106;
then B1 . x = the L_join of (EqRelLatt the Sorts of A) . x1,x2 by A16, FUNCT_1:72
.= x19 "\/" x29 by Def5 ;
then B1 . x is MSCongruence of A by Th17;
hence B1 . x in B by A6; :: thesis:

end;

then reconsider B1 = B1 as BinOp of B by A14, FUNCT_2:5;
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A19: 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:
A20: b in B by A6;
a in B by A6;
then A21: [a,b] in [:B,B:] by A20, ZFMISC_1:106;
hence B1 . a,b = the L_join of (EqRelLatt the Sorts of A) . a,b by FUNCT_1:72
.= a "\/" b by Def5 ;
:: thesis:
thus B2 . a,b = the L_meet of (EqRelLatt the Sorts of A) . a,b by A21, FUNCT_1:72
.= a /\ b by Def5 ; :: thesis:

end;

A22: now

let a, b be Element of B; :: thesis:
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
thus B1 . a,b = a9 "\/" b9 by A19
.= B1 . b,a by A19 ; :: thesis:

end;

A23: for a, b being Element of L holds a "\/" b = b "\/" a

proof

let a, b be Element of L; :: thesis:
thus a "\/" b = B1 . a,b by LATTICES:def 1
.= the L_join of L . b,a by A22
.= b "\/" a by LATTICES:def 1 ; :: thesis:

end;

A24: now

let a, b, c be Element of B; :: thesis:
reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;
reconsider e1 = b9 /\ c9 as MSCongruence of A by Th18;
reconsider e2 = a9 /\ b9 as MSCongruence of A by Th18;
thus B2 . a,(B2 . b,c) = B2 . a,e1 by A19
.= a9 /\ (b9 /\ c9) by A19
.= (a9 /\ b9) /\ c9 by PBOOLE:35
.= B2 . e2,c by A19
.= B2 . (B2 . a,b),c by A19 ; :: thesis:

end;

A25: 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:
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 A24
.= the L_meet of L . (a "/\" b),c by LATTICES:def 2
.= (a "/\" b) "/\" c by LATTICES:def 2 ; :: thesis:

end;

A26: now

let a, b, c be Element of B; :: thesis:
reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;
reconsider d = b9 "\/" c9 as MSCongruence of A by Th17;
reconsider e = a9 "\/" b9 as MSCongruence of A by Th17;
thus B1 . a,(B1 . b,c) = B1 . a,d by A19
.= a9 "\/" (b9 "\/" c9) by A19
.= (a9 "\/" b9) "\/" c9 by Th10
.= B1 . e,c by A19
.= B1 . (B1 . a,b),c by A19 ; :: thesis:

end;

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

end;

A28: now

let a, b be Element of B; :: thesis:
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
thus B2 . a,b = b9 /\ a9 by A19
.= B2 . b,a by A19 ; :: thesis:

end;

A29: for a, b being Element of L holds a "/\" b = b "/\" a

proof

let a, b be Element of L; :: thesis:
thus a "/\" b = B2 . a,b by LATTICES:def 2
.= the L_meet of L . b,a by A28
.= b "/\" a by LATTICES:def 2 ; :: thesis:

end;

A30: for a, b being Element of L holds a "/\" (a "\/" b) = a

proof

let a, b be Element of L; :: thesis:
A31: 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 Th17;
thus B2 . a,(B1 . a,b) = B2 . a,d by A19
.= a9 /\ (a9 "\/" b9) by A19
.= a by Th11 ; :: thesis:

end;

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

end;

for a, b being Element of L holds (a "/\" b) "\/" b = b

proof

let a, b be Element of L; :: thesis:
A32: 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 Th18;
thus B1 . (B2 . a,b),b = B1 . (a9 /\ b9),b9 by A19
.= EQR "\/" b9 by A19
.= b by Th12 ; :: thesis:

end;

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

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 A23, A27, A29, A25, A30, 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 A8, NAT_LAT:def 16;
take L ; :: thesis:
thus for x being set holds
( x in the carrier of L iff x is MSCongruence of A ) by A6; :: thesis: