theorem :: ROBBINS4:33

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