:: deftheorem Def1 defines orthomodular ROBBINS4:def 1 :
for L being non empty OrthoLattStr holds
( L is orthomodular iff for x, y being Element of L st x [= y holds
y = x "\/" ((x `) "/\" y) );