theorem Th24: :: YELLOW_7:24
for L being with_suprema Poset
for x, y being Element of (L opp) holds (~ x) "\/" (~ y) = x "/\" y