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-commutative & L is join-commutative ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; :: thesis: ( L is meet-commutative & L is join-commutative )
then A2: ( L is join-idempotent & L is meet-idempotent ) by Th1;
A3: for x, y being Element of L holds x "/\" y = y "/\" x

proof

let a, b be Element of L; :: thesis: a "/\" b = b "/\" a
a "/\" b = a "/\" (b "/\" (b "\/" a)) by A1
.= b "/\" (a "/\" (b "\/" a)) by A1
.= b "/\" (a "/\" (b "\/" (a "\/" a))) by A2, ROBBINS1:def 7
.= b "/\" (a "/\" (a "\/" (b "\/" a))) by A1
.= b "/\" a by A1 ;
hence a "/\" b = b "/\" a ; :: thesis: verum

end;

for x, y being Element of L holds x "\/" y = y "\/" x

proof

let a, b be Element of L; :: thesis: a "\/" b = b "\/" a
a "\/" b = a "\/" (b "\/" (b "/\" a)) by A1
.= b "\/" (a "\/" (b "/\" a)) by A1
.= b "\/" (a "\/" (b "/\" (a "/\" a))) by A2, SHEFFER1:def 9
.= b "\/" (a "\/" (a "/\" (b "/\" a))) by A1
.= b "\/" a by A1 ;
hence a "\/" b = b "\/" a ; :: thesis: verum

end;

hence ( L is meet-commutative & L is join-commutative ) by A3; :: thesis: verum