deffunc H₁( Element of S) -> set = bool [:(the Sorts of A . $1),(the Sorts of A . $1):];
consider M2 being ManySortedSet of such that
A1: for i being Element of the carrier of S holds M2 . i = H₁(i) from PBOOLE:sch 5();
defpred S₁[ set ] means $1 is MSCongruence of A;
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

proof

let C1 be MSCongruence of A; :: thesis: C1 in product M2
A4: dom C1 = the carrier of S by PARTFUN1:def 4
.= dom M2 by PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in dom M2 implies C1 . x in M2 . x )
assume x in dom M2 ; :: thesis: C1 . x in M2 . x
then reconsider x' = x as Element of the carrier of S by PARTFUN1:def 4;
A5: M2 . x' = bool [:(the Sorts of A . x'),(the Sorts of A . x'):] by A1;
C1 . x' is Subset of [:(the Sorts of A . x'),(the Sorts of A . x'):] ;
hence C1 . x in M2 . x by A5; :: thesis: verum

end;

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

end;

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

proof

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

proof

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

end;

end;

consider f being MSCongruence of A;
f in B by A6;
then reconsider B = B as non empty set ;
set D = the carrier of (EqRelLatt the Sorts of A);
set B1 = the L_join of (EqRelLatt the Sorts of A) || B;
set B2 = the L_meet of (EqRelLatt the Sorts of A) || B;
A8: B c= the carrier of (EqRelLatt the Sorts of A)

proof

now

let x be set ; :: 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;

hence B c= the carrier of (EqRelLatt the Sorts of A) by TARSKI:def 3; :: thesis: verum

end;

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 B1 = [:B,B:] by FUNCT_2:def 1;

now

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

end;

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

now

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

end;

then reconsider B2 = B2 as BinOp of B by A12, FUNCT_2:5;
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A15: 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 )
( a in B & b in B ) by A6;
then A16: [a,b] in [:B,B:] by 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: B2 . a,b = a /\ b
thus B2 . a,b = the L_meet of (EqRelLatt the Sorts of A) . a,b by A16, FUNCT_1:72
.= a /\ b by Def5 ; :: thesis: verum

end;

A17: B1 is commutative

proof

now

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

end;

hence B1 is commutative by BINOP_1:def 2; :: thesis: verum

end;

A18: B1 is associative

proof

now

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

end;

hence B1 is associative by BINOP_1:def 3; :: thesis: verum

end;

A19: B2 is commutative

proof

now

let a, b be Element of B; :: thesis: B2 . a,b = B2 . b,a
reconsider a' = a, b' = b as MSCongruence of A by A6;
thus B2 . a,b = b' /\ a' by A15
.= B2 . b,a by A15 ; :: thesis: verum

end;

hence B2 is commutative by BINOP_1:def 2; :: thesis: verum

end;

A20: B2 is associative

proof

now

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

end;

hence B2 is associative by BINOP_1:def 3; :: thesis: verum

end;

A21: 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 A17, BINOP_1:def 2
.= b "\/" a by LATTICES:def 1 ; :: thesis: verum

end;

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

end;

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

proof

reconsider a' = a, b' = b as MSCongruence of A by A6;
reconsider EQR = a' /\ b' as MSCongruence of A by Th18;
thus B1 . (B2 . a,b),b = B1 . (a' /\ b'),b' by A15
.= EQR "\/" b' by A15
.= b by Th12 ; :: thesis: verum

end;

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

end;

A25: 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 A19, BINOP_1:def 2
.= b "/\" a by LATTICES:def 2 ; :: 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_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 A20, BINOP_1:def 3
.= the L_meet of L . (a "/\" b),c by LATTICES:def 2
.= (a "/\" b) "/\" c 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
A27: B2 . a,(B1 . a,b) = a

proof

reconsider a' = a, b' = b as MSCongruence of A by A6;
reconsider d = a' "\/" b' as MSCongruence of A by Th17;
thus B2 . a,(B1 . a,b) = B2 . a,d by A15
.= a' /\ (a' "\/" b') by A15
.= a by Th11 ; :: thesis: verum

end;

thus a "/\" (a "\/" b) = the L_meet of L . a,(a "\/" b) by LATTICES:def 2
.= a by A27, 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 A21, A22, A23, A25, A26, 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: 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