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