theorem :: ROBBINS4:32

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