theorem Th39: :: WAYBEL27:39

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