theorem Th37: :: WAYBEL27:37

for S, T being complete LATTICE
for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f))