let L be non empty LattStr ; :: thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-associative & L is join-associative ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; :: thesis: ( L is meet-associative & L is join-associative )
then A2: ( L is meet-commutative & L is join-commutative ) by Th2;
A3: for x, y, z being Element of L holds x "\/" (y "\/" z) = (x "\/" y) "\/" z
proof
let a, b, c be Element of L; :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
a "\/" (b "\/" c) = a "\/" (c "\/" b) by A2
.= c "\/" (a "\/" b) by A1
.= (a "\/" b) "\/" c by A2 ;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; :: thesis: verum
end;
for x, y, z being Element of L holds x "/\" (y "/\" z) = (x "/\" y) "/\" z
proof
let a, b, c be Element of L; :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
a "/\" (b "/\" c) = a "/\" (c "/\" b) by A2
.= c "/\" (a "/\" b) by A1
.= (a "/\" b) "/\" c by A2 ;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; :: thesis: verum
end;
hence ( L is meet-associative & L is join-associative ) by A3; :: thesis: verum