set L = the 1 -element Ortholattice;
take the 1 -element Ortholattice ; :: thesis: ( the 1 -element Ortholattice is join-Associative & the 1 -element Ortholattice is meet-Absorbing & the 1 -element Ortholattice is de_Morgan & the 1 -element Ortholattice is orthomodular )
thus ( the 1 -element Ortholattice is join-Associative & the 1 -element Ortholattice is meet-Absorbing & the 1 -element Ortholattice is de_Morgan & the 1 -element Ortholattice is orthomodular ) ; :: thesis: verum