theorem Th30: :: ROBBINS3:30

for L being non empty OrthoLattStr st L is Boolean & L is well-complemented & L is Lattice-like holds
L is Ortholattice