theorem :: WAYBEL34:19

for W being with_non-empty_element set holds
( (W LowerAdj) * (W UpperAdj) = id (W -SUP_category) & (W UpperAdj) * (W LowerAdj) = id (W -INF_category) )