:: deftheorem Def4 defines UPS WAYBEL27:def 4 :
for S being non empty RelStr
for T being non empty reflexive antisymmetric RelStr
for b₃ being strict RelStr holds
( b₃ = UPS (S,T) iff ( b₃ is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b₃ iff x is directed-sups-preserving Function of S,T ) ) ) );