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

proof

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;

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