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