let L be non empty join-associative meet-commutative meet-absorbing join-absorbing OrthoLattStr ; :: thesis: ( L is Orthomodular implies L is orthomodular )

assume A1: L is Orthomodular ; :: thesis: L is orthomodular

let x, y be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )

assume x [= y ; :: thesis: y = x "\/" ((x `) "/\" y)

then x "\/" y = y ;

hence y = x "\/" ((x `) "/\" y) by A1; :: thesis: verum

assume A1: L is Orthomodular ; :: thesis: L is orthomodular

let x, y be Element of L; :: according to ROBBINS4:def 1 :: thesis: ( x [= y implies y = x "\/" ((x `) "/\" y) )

assume x [= y ; :: thesis: y = x "\/" ((x `) "/\" y)

then x "\/" y = y ;

hence y = x "\/" ((x `) "/\" y) by A1; :: thesis: verum