let L be non empty join-commutative meet-commutative meet-absorbing join-absorbing distributive join-idempotent LattStr ; :: thesis: L is join-associative
let x, y, z be Element of L; :: according to LATTICES:def 5 :: thesis: x "\/" (y "\/" z) = (x "\/" y) "\/" z
A1: ((y "\/" z) "\/" x) "/\" y = (y "/\" (y "\/" z)) "\/" (y "/\" x) by LATTICES:def 11
.= ((y "/\" y) "\/" (y "/\" z)) "\/" (y "/\" x) by LATTICES:def 11
.= (y "\/" (y "/\" z)) "\/" (y "/\" x)
.= y "\/" (y "/\" x) by LATTICES:def 8
.= y by LATTICES:def 8 ;
A2: ((x "\/" y) "\/" z) "/\" x = x by Th6;
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 LATTICES:def 11
.= ((x "\/" y) "/\" (x "\/" (y "\/" z))) "\/" z by Th6
.= ((x "/\" (x "\/" (y "\/" z))) "\/" (y "/\" (x "\/" (y "\/" z)))) "\/" z by LATTICES:def 11
.= (x "\/" y) "\/" z by A1, LATTICES:def 9 ;
((x "\/" y) "\/" z) "/\" (x "\/" (y "\/" z)) = (((x "\/" y) "\/" z) "/\" x) "\/" (((x "\/" y) "\/" z) "/\" (y "\/" z)) by LATTICES:def 11
.= x "\/" ((((x "\/" y) "\/" z) "/\" y) "\/" (((x "\/" y) "\/" z) "/\" z)) by A2, LATTICES:def 11
.= x "\/" (y "\/" (((x "\/" y) "\/" z) "/\" z)) by Th6
.= x "\/" (y "\/" (((x "\/" y) "/\" z) "\/" (z "/\" z))) by LATTICES:def 11
.= x "\/" (y "\/" (((x "\/" y) "/\" z) "\/" z))
.= x "\/" (y "\/" z) by LATTICES:def 8 ;
hence x "\/" (y "\/" z) = (x "\/" y) "\/" z by A3; :: thesis: verum
end;
hence x "\/" (y "\/" z) = (x "\/" y) "\/" z ; :: thesis: verum