theorem :: ROBBINS4:39

for L being non empty OrthoLattStr holds
( L is Orthomodular_Lattice iff ( L is join-Associative & L is meet-Absorbing & L is de_Morgan & L is Orthomodular ) )