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