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 ~ )