theorem Th10: :: WAYBEL34:10

for S, T being complete LATTICE
for g being infs-preserving Function of S,T holds UpperAdj (LowerAdj g) = g