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