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