set L = the 1 -element Ortholattice;
the 1 -element Ortholattice is orthomodular by STRUCT_0:def 10;
hence ex b₁ being Ortholattice st
( b₁ is trivial & b₁ is orthomodular & b₁ is modular & b₁ is Boolean ) ; :: thesis: verum