theorem Th35: :: YELLOW_7:35
for L being bounded LATTICE
for x, y being Element of L holds
( y is_a_complement_of x iff y ~ is_a_complement_of x ~ )