for L being Ortholattice
for a, b, c being Element of L st a _|_ b & a _|_ c holds
( a _|_ b "/\" c & a _|_ b "\/" c )