let L be non empty OrthoLattStr ; :: thesis: ( L is join-associative & L is join-commutative & L is de_Morgan implies L is meet-commutative )
assume ( L is join-associative & L is join-commutative & L is de_Morgan ) ; :: thesis: L is meet-commutative
then reconsider L1 = L as non empty join-commutative join-associative de_Morgan OrthoLattStr ;
let a, b be Element of L; :: according to LATTICES:def 6 :: thesis: a "/\" b = b "/\" a
reconsider a1 = a, b1 = b as Element of L1 ;
thus a "/\" b = a1 *' b1 by Def23
.= b1 *' a1
.= b "/\" a by Def23 ; :: thesis: verum