set B = { x where x is Relation of X,X : x is Equivalence_Relation of X } ;
id X in { x where x is Relation of X,X : x is Equivalence_Relation of X } ;
then reconsider B = { x where x is Relation of X,X : x is Equivalence_Relation of X } as non empty set ;
defpred S1[ Element of B, Element of B, Element of B] means ( $1 \/ $2 c= $3 & ( for x' being Element of B st $1 \/ $2 c= x' holds
$3 c= x' ) );
A1: for x, y being Element of B ex z being Element of B st S1[x,y,z]
proof
let x, y be Element of B; :: thesis: ex z being Element of B st S1[x,y,z]
A2: ( x in B & y in B ) ;
then A3: ex x'' being Relation of X,X st
( x = x'' & x'' is Equivalence_Relation of X ) ;
ex y'' being Relation of X,X st
( y = y'' & y'' is Equivalence_Relation of X ) by A2;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A3;
consider z being Equivalence_Relation of X such that
A4: ( x1 \/ y1 c= z & ( for x' being Equivalence_Relation of X st x1 \/ y1 c= x' holds
z c= x' ) ) by EQREL_1:20;
z in B ;
then reconsider z' = z as Element of B ;
take z' ; :: thesis: S1[x,y,z']
thus x \/ y c= z' by A4; :: thesis: for x' being Element of B st x \/ y c= x' holds
z' c= x'
hereby :: thesis: verum
let x' be Element of B; :: thesis: ( x \/ y c= x' implies z' c= x' )
assume A5: x \/ y c= x' ; :: thesis: z' c= x'
x' in B ;
then ex x'' being Relation of X,X st
( x' = x'' & x'' is Equivalence_Relation of X ) ;
then reconsider x1' = x' as Equivalence_Relation of X ;
x \/ y c= x1' by A5;
hence z' c= x' by A4; :: thesis: verum
end;
end;
consider B1 being BinOp of B such that
A6: for x, y being Element of B holds S1[x,y,B1 . x,y] from BINOP_1:sch 3(A1);
A7: now
let x, y be Equivalence_Relation of X; :: thesis: B1 . x,y = x "\/" y
( x in B & y in B ) ;
then reconsider x1 = x, y1 = y as Element of B ;
reconsider B1' = B1 . x1,y1 as Element of B ;
B1' in B ;
then ex B1'' being Relation of X,X st
( B1' = B1'' & B1'' is Equivalence_Relation of X ) ;
then reconsider B1' = B1' as Equivalence_Relation of X ;
A8: ( x1 \/ y1 c= B1 . x1,y1 & ( for x' being Element of B st x1 \/ y1 c= x' holds
B1 . x1,y1 c= x' ) ) by A6;
now
let x' be Equivalence_Relation of X; :: thesis: ( x \/ y c= x' implies B1 . x,y c= x' )
assume A9: x \/ y c= x' ; :: thesis: B1 . x,y c= x'
x' in B ;
then reconsider x1' = x' as Element of B ;
x \/ y c= x1' by A9;
hence B1 . x,y c= x' by A8; :: thesis: verum
end;
then B1' = x "\/" y by A8, EQREL_1:def 3;
hence B1 . x,y = x "\/" y ; :: thesis: verum
end;
defpred S2[ Element of B, Element of B, Element of B] means $3 = $1 /\ $2;
A10: 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]
A11: ( x in B & y in B ) ;
then A12: ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) ;
ex y1 being Relation of X,X st
( y = y1 & y1 is Equivalence_Relation of X ) by A11;
then reconsider x' = x, y' = y as Equivalence_Relation of X by A12;
set z = x' /\ y';
x' /\ y' in B ;
then reconsider z = x' /\ y' as Element of B ;
take z ; :: thesis: S2[x,y,z]
thus S2[x,y,z] ; :: thesis: verum
end;
consider B2 being BinOp of B such that
A13: for x, y being Element of B holds S2[x,y,B2 . x,y] from BINOP_1:sch 3(A10);
A14: now
let x, y be Equivalence_Relation of X; :: thesis: B2 . x,y = x /\ y
( x in B & y in B ) ;
then reconsider x' = x, y' = y as Element of B ;
B2 . x',y' = x' /\ y' by A13;
hence B2 . x,y = x /\ y ; :: thesis: verum
end;
reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;
A15: B1 is commutative
proof
now
let a, b be Element of B; :: thesis: B1 . a,b = B1 . b,a
A16: ( a in B & b in B ) ;
then A17: ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) by A16;
then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A17;
thus B1 . a,b = U2 "\/" U1 by A7
.= B1 . b,a by A7 ; :: 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
A19: ( a in B & b in B & c in B ) ;
then A20: ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
A21: ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) by A19;
ex x3 being Relation of X,X st
( c = x3 & x3 is Equivalence_Relation of X ) by A19;
then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A20, A21;
thus B1 . a,(B1 . b,c) = B1 . a,(U2 "\/" U3) by A7
.= U1 "\/" (U2 "\/" U3) by A7
.= (U1 "\/" U2) "\/" U3 by EQREL_1:21
.= B1 . (U1 "\/" U2),c by A7
.= B1 . (B1 . a,b),c by A7 ; :: thesis: verum
end;
hence B1 is associative by BINOP_1:def 3; :: thesis: verum
end;
A22: B2 is commutative
proof
now
let a, b be Element of B; :: thesis: B2 . a,b = B2 . b,a
A23: ( a in B & b in B ) ;
then A24: ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) by A23;
then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A24;
thus B2 . a,b = U2 /\ U1 by A14
.= B2 . b,a by A14 ; :: thesis: verum
end;
hence B2 is commutative by BINOP_1:def 2; :: thesis: verum
end;
A25: B2 is associative
proof
now
let a, b, c be Element of B; :: thesis: B2 . a,(B2 . b,c) = B2 . (B2 . a,b),c
A26: ( a in B & b in B & c in B ) ;
then A27: ex x1 being Relation of X,X st
( a = x1 & x1 is Equivalence_Relation of X ) ;
A28: ex x2 being Relation of X,X st
( b = x2 & x2 is Equivalence_Relation of X ) by A26;
ex x3 being Relation of X,X st
( c = x3 & x3 is Equivalence_Relation of X ) by A26;
then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by A27, A28;
thus B2 . a,(B2 . b,c) = B2 . a,(U2 /\ U3) by A14
.= U1 /\ (U2 /\ U3) by A14
.= (U1 /\ U2) /\ U3 by XBOOLE_1:16
.= B2 . (U1 /\ U2),c by A14
.= B2 . (B2 . a,b),c by A14 ; :: thesis: verum
end;
hence B2 is associative by BINOP_1:def 3; :: thesis: verum
end;
A29: 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 A15, BINOP_1:def 2
.= b "\/" a by LATTICES:def 1 ; :: thesis: verum
end;
A30: 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 ;
A31: 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 A18, BINOP_1:def 3
.= (a "\/" b) "\/" c by A31, LATTICES:def 1 ; :: thesis: verum
end;
A32: 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 ;
A33: B1 . (B2 . x,y),y = y
proof
A34: ( x in B & y in B ) ;
then A35: ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) ;
ex x2 being Relation of X,X st
( y = x2 & x2 is Equivalence_Relation of X ) by A34;
then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A35;
B2 . x,y = U1 /\ U2 by A14;
hence B1 . (B2 . x,y),y = U2 "\/" (U1 /\ U2) by A7
.= y by EQREL_1:25 ;
:: thesis: verum
end;
thus (a "/\" b) "\/" b = the L_join of L . (a "/\" b),b by LATTICES:def 1
.= b by A33, LATTICES:def 2 ; :: thesis: verum
end;
A36: 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 A22, BINOP_1:def 2
.= b "/\" a by LATTICES:def 2 ; :: thesis: verum
end;
A37: 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 ;
A38: 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 A25, BINOP_1:def 3
.= (a "/\" b) "/\" c by A38, 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 ;
A39: B2 . x,(B1 . x,y) = x
proof
A40: ( x in B & y in B ) ;
then A41: ex x1 being Relation of X,X st
( x = x1 & x1 is Equivalence_Relation of X ) ;
ex x2 being Relation of X,X st
( y = x2 & x2 is Equivalence_Relation of X ) by A40;
then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A41;
B1 . x,y = U1 "\/" U2 by A7;
hence B2 . x,(B1 . x,y) = U1 /\ (U1 "\/" U2) by A14
.= x by EQREL_1:24 ;
:: thesis: verum
end;
thus a "/\" (a "\/" b) = the L_meet of L . a,(a "\/" b) by LATTICES:def 2
.= a by A39, 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 A29, A30, A32, A36, A37, 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: ( the carrier of L = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of L . x,y = x /\ y & the L_join of L . x,y = x "\/" y ) ) )
thus the carrier of L = { x where x is Relation of X,X : x is Equivalence_Relation of X } ; :: thesis: for x, y being Equivalence_Relation of X holds
( the L_meet of L . x,y = x /\ y & the L_join of L . x,y = x "\/" y )
thus for x, y being Equivalence_Relation of X holds
( the L_meet of L . x,y = x /\ y & the L_join of L . x,y = x "\/" y ) by A7, A14; :: thesis: verum