set f = the directed-sups-preserving Function of S,T;
the directed-sups-preserving Function of S,T 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