theorem :: ROBBINS4:37

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