theorem Th34: :: ROBBINS4:34

for L being Ortholattice holds
( L is orthomodular iff for a, b being Element of L st b [= a holds
a "/\" ((a `) "\/" b) = b )