:: deftheorem defines are_orthogonal ROBBINS4:def 5 :
for L being Ortholattice
for a, b being Element of L holds
( a,b are_orthogonal iff a [= b ` );