:: deftheorem Def5 defines UPS WAYBEL27:def 5 :
for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr
for f being Function of S1,S2 st f is directed-sups-preserving holds
for g being Function of T1,T2 st g is directed-sups-preserving holds
for b₇ being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds
( b₇ = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b₇ . h = (g * h) * f );