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 S_{1}[ 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 S_{1}[x,y,z]

A6: for x, y being Element of B holds S_{1}[x,y,B1 . (x,y)]
from BINOP_1:sch 3(A1);

defpred S_{2}[ 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 S_{2}[x,y,z]

A9: for x, y being Element of B holds S_{2}[x,y,B2 . (x,y)]
from BINOP_1:sch 3(A7);

reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;

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

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 S

$3 c= x9 ) );

A1: for x, y being Element of B ex z being Element of B st S

proof

consider B1 being BinOp of B such that
let x, y be Element of B; :: thesis: ex z being Element of B st S_{1}[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:12;

z in B ;

then reconsider z9 = z as Element of B ;

take z9 ; :: thesis: S_{1}[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

end;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:12;

z in B ;

then reconsider z9 = z as Element of B ;

take z9 ; :: thesis: S

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;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

A6: for x, y being Element of B holds S

defpred S

A7: for x, y being Element of B ex z being Element of B st S

proof

consider B2 being BinOp of B such that
let x, y be Element of B; :: thesis: ex z being Element of B st S_{2}[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: S_{2}[x,y,z]

thus S_{2}[x,y,z]
; :: thesis: verum

end;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: S

thus S

A9: for x, y being Element of B holds S

reconsider L = LattStr(# B,B1,B2 #) as non empty LattStr ;

A10: now :: thesis: for x, y being Equivalence_Relation of X holds B1 . (x,y) = x "\/" y

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;

then B19 = x "\/" y by A13, EQREL_1:def 2;

hence B1 . (x,y) = x "\/" y ; :: thesis: verum

end;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 :: thesis: for x9 being Equivalence_Relation of X st x \/ y c= x9 holds

B1 . (x,y) c= x9

x1 \/ y1 c= B1 . (x1,y1)
by A6;B1 . (x,y) c= x9

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;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

then B19 = x "\/" y by A13, EQREL_1:def 2;

hence B1 . (x,y) = x "\/" y ; :: thesis: verum

A15: now :: thesis: for a, b, c being Element of B holds B1 . (a,(B1 . (b,c))) = B1 . ((B1 . (a,b)),c)

A18:
for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
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:13

.= B1 . ((U1 "\/" U2),c) by A10

.= B1 . ((B1 . (a,b)),c) by A10 ; :: thesis: verum

end;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:13

.= B1 . ((U1 "\/" U2),c) by A10

.= B1 . ((B1 . (a,b)),c) by A10 ; :: thesis: verum

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;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

A20: now :: thesis: for a, b being Element of B holds B1 . (a,b) = B1 . (b,a)

A22:
for a, b being Element of L holds a "\/" b = b "\/" a
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;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

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;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

A23: now :: thesis: for x, y being Equivalence_Relation of X holds B2 . (x,y) = x /\ y

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;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

A25: now :: thesis: for a, b, c being Element of B holds B2 . (a,(B2 . (b,c))) = B2 . ((B2 . (a,b)),c)

A28:
for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
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;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

proof

A30:
for a, b being Element of L holds a "/\" (a "\/" b) = a
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;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

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

.= a by A31, LATTICES:def 1 ; :: thesis: verum

end;reconsider x = a, y = b as Element of B ;

A31: B2 . (x,(B1 . (x,y))) = x

proof

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

:: thesis: verum

end;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:16 ;

:: thesis: verum

.= a by A31, LATTICES:def 1 ; :: thesis: verum

A33: now :: thesis: for a, b being Element of B holds B2 . (a,b) = B2 . (b,a)

A35:
for a, b being Element of L holds a "/\" b = b "/\" a
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;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

proof

for a, b being Element of L holds (a "/\" b) "\/" b = b
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;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

proof

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;
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

.= b by A36, LATTICES:def 2 ; :: thesis: verum

end;reconsider x = a, y = b as Element of B ;

A36: B1 . ((B2 . (x,y)),y) = y

proof

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

:: thesis: verum

end;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:17 ;

:: thesis: verum

.= b by A36, LATTICES:def 2 ; :: thesis: verum

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