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 A1: ( L is join-associative & L is join-commutative & L is de_Morgan ) ; :: thesis: L is meet-commutative
let a, b be Element of L; :: according to LATTICES:def 6 :: thesis: a "/\" b = b "/\" a
thus a "/\" b = a *' b by A1, Def23
.= b *' a by A1, Th8
.= b "/\" a by A1, Def23 ; :: thesis: verum