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