theorem Th21: :: YELLOW_7:21

for L being with_infima Poset
for x, y being Element of L holds x "/\" y = (x ~) "\/" (y ~)