theorem Th40: :: WAYBEL27:40

for X being non empty set
for S, T being non empty Poset
for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)