consider f being directed-sups-preserving Function of S,T;
f in the carrier of (UPS S,T) by Def4;
then UPS S,T is non empty full SubRelStr of T |^ the carrier of S by Def4;
hence ( not UPS S,T is empty & UPS S,T is reflexive & UPS S,T is antisymmetric & UPS S,T is constituted-Functions ) ; :: thesis: verum