let L be modular Ortholattice; :: 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 "\/" ((x `) "/\" y) = (x "\/" (x `)) "/\" y by LATTICES:def 12;

then x "\/" ((x `) "/\" y) = (y "\/" (y `)) "/\" y by ROBBINS3:def 7;

hence y = x "\/" ((x `) "/\" y) by LATTICES:def 9; :: thesis: verum

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 "\/" ((x `) "/\" y) = (x "\/" (x `)) "/\" y by LATTICES:def 12;

then x "\/" ((x `) "/\" y) = (y "\/" (y `)) "/\" y by ROBBINS3:def 7;

hence y = x "\/" ((x `) "/\" y) by LATTICES:def 9; :: thesis: verum