theorem Th59: :: ROBBINS1:59

for L being non empty join-commutative meet-commutative well-complemented OrthoLattStr
for x being Element of L holds
( x + (x `) = Top L & x "/\" (x `) = Bottom L )