deffunc H1( Element of I) -> set = bool [:(M . $1),(M . $1):];
consider M2 being ManySortedSet of such that
A1: for i being Element of I holds M2 . i = H1(i) from PBOOLE:sch 5();
 defpred S1[ set ] means $1 is Equivalence_Relation of M;
consider B being set such that
A2: for x being set holds
( x in B iff ( x in product M2 & S1[x] ) ) from XBOOLE_0:sch 1();
 A3: for EqR being Equivalence_Relation of M holds EqR in product M2
proof
let EqR be Equivalence_Relation of M; :: thesis: EqR in product M2
A4: dom EqR = I by PARTFUN1:def 4
.= dom M2 by PARTFUN1:def 4 ;
for x being set st x in dom M2 holds
EqR . x in M2 . x
proof
let x be set ; :: thesis: ( x in dom M2 implies EqR . x in M2 . x )
assume x in dom M2 ; :: thesis: EqR . x in M2 . x
then reconsider x' = x as Element of I by PARTFUN1:def 4;
A5: M2 . x' = bool [:(M . x'),(M . x'):] by A1;
EqR . x' is Subset of [:(M . x'),(M . x'):] ;
hence EqR . x in M2 . x by A5; :: thesis: verum
end;
hence EqR in product M2 by A4, CARD_3:18; :: thesis: verum
end;
consider f being Equivalence_Relation of M;
f in product M2 by A3;
then reconsider B = B as non empty set by A2;
defpred S2[ 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 S2[x,y,z]
proof
let x, y be Element of B; :: thesis: ex z being Element of B st S2[x,y,z]
reconsider x' = x, y' = y as Equivalence_Relation of M by A2;
set z = x' "\/" y';
x' "\/" y' in product M2 by A3;
then reconsider z = x' "\/" y' as Element of B by A2;
take z ; :: thesis: S2[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 ( x1 = x & y1 = y ) ; :: thesis: ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 \/ y1 & z = EqCl EqR3 )
hence ex EqR3 being ManySortedRelation of M st
( EqR3 = x1 \/ y1 & z = EqCl EqR3 ) by Def4; :: thesis: verum
end;
consider B1 being BinOp of B such that
A7: for x, y being Element of B holds S2[x,y,B1 . x,y] from BINOP_1:sch 3(A6);
A8: now
let x, y be Equivalence_Relation of M; :: thesis: B1 . x,y = x "\/" y
( x in product M2 & y in product M2 ) by A3;
then reconsider x' = x, y' = y as Element of B by A2;
consider EqR3 being ManySortedRelation of M such that
A9: ( EqR3 = x \/ y & B1 . x',y' = EqCl EqR3 ) by A7;
thus B1 . x,y = x "\/" y by A9, Def4; :: thesis: verum
end;
defpred S3[ 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 S3[x,y,z]
proof
let x, y be Element of B; :: thesis: ex z being Element of B st S3[x,y,z]
reconsider x' = x, y' = y as Equivalence_Relation of M by A2;
set z = x' /\ y';
for i being set st i in I holds
(x' /\ y') . i is Relation of (M . i)
proof
let i be set ; :: thesis: ( i in I implies (x' /\ y') . i is Relation of (M . i) )
assume i in I ; :: thesis: (x' /\ y') . i is Relation of (M . i)
then reconsider i' = i as Element of I ;
(x' /\ y') . i = (x' . i') /\ (y' . i') by PBOOLE:def 8;
hence (x' /\ y') . i is Relation of (M . i) ; :: thesis: verum
end;
then reconsider z = x' /\ y' as ManySortedRelation of M by MSUALG_4:def 2;
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
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 A11: ( i in I & z . i = R ) ; :: thesis: R is Equivalence_Relation of (M . i)
then reconsider i' = i as Element of I ;
reconsider x1'' = x' . i', y1'' = y' . i' as Relation of (M . i) ;
reconsider x'' = x1'', y'' = y1'' as Equivalence_Relation of (M . i) by MSUALG_4:def 3;
R = x'' /\ y'' by A11, PBOOLE:def 8;
hence R is Equivalence_Relation of (M . i) ; :: thesis: verum
end;
then reconsider z = z as Equivalence_Relation of M by MSUALG_4:def 3;
z in product M2 by A3;
then reconsider z = z as Element of B by A2;
take z ; :: thesis: S3[x,y,z]
thus S3[x,y,z] ; :: thesis: verum
end;
consider B2 being BinOp of B such that
A12: for x, y being Element of B holds S3[x,y,B2 . x,y] from BINOP_1:sch 3(A10);
A13: now
let x, y be Equivalence_Relation of M; :: thesis: B2 . x,y = x /\ y
( x in product M2 & y in product M2 ) by A3;
then reconsider x' = x, y' = y as Element of B by A2;
( x' = x & y' = y ) ;
hence B2 . x,y = x /\ y by A12; :: thesis: verum
end;
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A14: B1 is commutative
proof
now
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 A8
.= B1 . b,a by A8 ; :: thesis: verum
end;
hence B1 is commutative by BINOP_1:def 2; :: thesis: verum
end;
A15: 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 U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;
thus B1 . a,(B1 . b,c) = B1 . a,(U2 "\/" U3) by A8
.= U1 "\/" (U2 "\/" U3) by A8
.= (U1 "\/" U2) "\/" U3 by Th10
.= B1 . (U1 "\/" U2),c by A8
.= B1 . (B1 . a,b),c by A8 ; :: thesis: verum
end;
hence B1 is associative by BINOP_1:def 3; :: thesis: verum
end;
A16: B2 is commutative
proof
now
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 A13
.= B2 . b,a by A13 ; :: thesis: verum
end;
hence B2 is commutative by BINOP_1:def 2; :: thesis: verum
end;
A17: 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 U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;
reconsider EQR1 = U2 /\ U3 as Equivalence_Relation of M by Th13;
reconsider EQR2 = U1 /\ U2 as Equivalence_Relation of M by Th13;
thus B2 . a,(B2 . b,c) = B2 . a,EQR1 by A13
.= U1 /\ (U2 /\ U3) by A13
.= (U1 /\ U2) /\ U3 by PBOOLE:35
.= B2 . EQR2,c by A13
.= B2 . (B2 . a,b),c by A13 ; :: thesis: verum
end;
hence B2 is associative by BINOP_1:def 3; :: thesis: verum
end;
A18: 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
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 A14, BINOP_1:def 2
.= b "\/" a by LATTICES:def 1 ; :: thesis: verum
end;
A19: 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
reconsider x = a, y = b, z = c as Element of B ;
A20: 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 A15, BINOP_1:def 3
.= (a "\/" b) "\/" c by A20, LATTICES:def 1 ; :: thesis: verum
end;
A21: 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
reconsider x = a, y = b as Element of B ;
A22: B1 . (B2 . x,y),y = y
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
reconsider EQR = U1 /\ U2 as Equivalence_Relation of M by Th13;
B2 . x,y = U1 /\ U2 by A13;
hence B1 . (B2 . x,y),y = EQR "\/" U2 by A8
.= y by Th12 ;
:: thesis: verum
end;
thus (a "/\" b) "\/" b = the L_join of L . (a "/\" b),b by LATTICES:def 1
.= b by A22, LATTICES:def 2 ; :: thesis: verum
end;
A23: 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
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 A16, BINOP_1:def 2
.= b "/\" a by LATTICES:def 2 ; :: 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
reconsider x = a, y = b, z = c as Element of B ;
A25: 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 A17, BINOP_1:def 3
.= (a "/\" b) "/\" c by A25, 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
reconsider x = a, y = b as Element of B ;
A26: B2 . x,(B1 . x,y) = x
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
B1 . x,y = U1 "\/" U2 by A8;
hence B2 . x,(B1 . x,y) = U1 /\ (U1 "\/" U2) by A13
.= x by Th11 ;
:: thesis: verum
end;
thus a "/\" (a "\/" b) = the L_meet of L . a,(a "\/" b) by LATTICES:def 2
.= a by A26, 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 A18, A19, A21, A23, A24, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
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 ) :: 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 )
proof
let x be set ; :: thesis: ( x in the carrier of L iff x is Equivalence_Relation of M )
thus ( x in the carrier of L implies x is Equivalence_Relation of M ) by A2; :: thesis: ( x is Equivalence_Relation of M implies x in the carrier of L )
thus ( x is Equivalence_Relation of M implies x in the carrier of L ) :: thesis: verum
proof
assume A27: x is Equivalence_Relation of M ; :: thesis: x in the carrier of L
then x in product M2 by A3;
hence x in the carrier of L by A2, A27; :: thesis: verum
end;
end;
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 A8, A13; :: thesis: verum