let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing join-idempotent distributive' LattStr ; :: thesis: L is meet-associative

let x, y, z be Element of L; :: according to LATTICES:def 7 :: thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z

A1: ((x "/\" y) "/\" z) "\/" x = x by Th7;

A2: ((y "/\" z) "/\" x) "\/" y = (y "\/" (y "/\" z)) "/\" (y "\/" x) by Def5

.= ((y "\/" y) "/\" (y "\/" z)) "/\" (y "\/" x) by Def5

.= (y "/\" (y "\/" z)) "/\" (y "\/" x)

.= y "/\" (y "\/" x) by LATTICES:def 9

.= y by LATTICES:def 9 ;

x "/\" (y "/\" z) = (x "/\" y) "/\" z

let x, y, z be Element of L; :: according to LATTICES:def 7 :: thesis: x "/\" (y "/\" z) = (x "/\" y) "/\" z

A1: ((x "/\" y) "/\" z) "\/" x = x by Th7;

A2: ((y "/\" z) "/\" x) "\/" y = (y "\/" (y "/\" z)) "/\" (y "\/" x) by Def5

.= ((y "\/" y) "/\" (y "\/" z)) "/\" (y "\/" x) by Def5

.= (y "/\" (y "\/" z)) "/\" (y "\/" x)

.= y "/\" (y "\/" x) by LATTICES:def 9

.= y by LATTICES:def 9 ;

x "/\" (y "/\" z) = (x "/\" y) "/\" z

proof

hence
x "/\" (y "/\" z) = (x "/\" y) "/\" z
; :: thesis: verum
set A = ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z));

A3: ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" (z "\/" (x "/\" (y "/\" z))) by Def5

.= ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" z by Th7

.= ((x "\/" (x "/\" (y "/\" z))) "/\" (y "\/" (x "/\" (y "/\" z)))) "/\" z by Def5

.= (x "/\" y) "/\" z by A2, LATTICES:def 8 ;

((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = (((x "/\" y) "/\" z) "\/" x) "/\" (((x "/\" y) "/\" z) "\/" (y "/\" z)) by Def5

.= x "/\" ((((x "/\" y) "/\" z) "\/" y) "/\" (((x "/\" y) "/\" z) "\/" z)) by A1, Def5

.= x "/\" (y "/\" (((x "/\" y) "/\" z) "\/" z)) by Th7

.= x "/\" (y "/\" (((x "/\" y) "\/" z) "/\" (z "\/" z))) by Def5

.= x "/\" (y "/\" (((x "/\" y) "\/" z) "/\" z))

.= x "/\" (y "/\" z) by LATTICES:def 9 ;

hence x "/\" (y "/\" z) = (x "/\" y) "/\" z by A3; :: thesis: verum

end;A3: ((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" (z "\/" (x "/\" (y "/\" z))) by Def5

.= ((x "/\" y) "\/" (x "/\" (y "/\" z))) "/\" z by Th7

.= ((x "\/" (x "/\" (y "/\" z))) "/\" (y "\/" (x "/\" (y "/\" z)))) "/\" z by Def5

.= (x "/\" y) "/\" z by A2, LATTICES:def 8 ;

((x "/\" y) "/\" z) "\/" (x "/\" (y "/\" z)) = (((x "/\" y) "/\" z) "\/" x) "/\" (((x "/\" y) "/\" z) "\/" (y "/\" z)) by Def5

.= x "/\" ((((x "/\" y) "/\" z) "\/" y) "/\" (((x "/\" y) "/\" z) "\/" z)) by A1, Def5

.= x "/\" (y "/\" (((x "/\" y) "/\" z) "\/" z)) by Th7

.= x "/\" (y "/\" (((x "/\" y) "\/" z) "/\" (z "\/" z))) by Def5

.= x "/\" (y "/\" (((x "/\" y) "\/" z) "/\" z))

.= x "/\" (y "/\" z) by LATTICES:def 9 ;

hence x "/\" (y "/\" z) = (x "/\" y) "/\" z by A3; :: thesis: verum