:: deftheorem Def2 defines Orthomodular ROBBINS4:def 2 :
for L being non empty OrthoLattStr holds
( L is Orthomodular iff for x, y being Element of L holds x "\/" ((x `) "/\" (x "\/" y)) = x "\/" y );