theorem Th18: :: WAYBEL34:18

for W being with_non-empty_element set holds
( (W LowerAdj) " = W UpperAdj & (W UpperAdj) " = W LowerAdj )