UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4;
hence UPS (S,T) is transitive ; :: thesis: verum