theorem :: ROBBINS4:30

for L being Ortholattice
for a being Element of L holds
( a _|_ a iff a = Bottom L )