let L be non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr ; :: thesis: ( L is orthomodular implies L is Orthomodular )
assume L is orthomodular ; :: thesis: L is Orthomodular
then for x, y being Element of L holds x "\/" ((x ` ) "/\" (x "\/" y)) = x "\/" y by tw1;
hence L is Orthomodular by DefMod3; :: thesis: verum