theorem Th2: :: ROBBINS4:2

for L being Ortholattice
for a being Element of L holds
( a "\/" (a `) = Top L & a "/\" (a `) = Bottom L )