consider L being trivial Ortholattice;
L is orthomodular

proof

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

end;

hence ex b₁ being Ortholattice st
( b₁ is trivial & b₁ is orthomodular & b₁ is modular & b₁ is Boolean ) ; :: thesis: verum