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

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

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