theorem Th9: :: WAYBEL34:9

for L1, L2, L3 being complete LATTICE
for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)