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