theorem Th36: :: ROBBINS4:36

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