let S be non empty RelStr ; :: thesis: for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS S,T) c= Funcs the carrier of S,the carrier of T
let T be non empty reflexive antisymmetric RelStr ; :: thesis: the carrier of (UPS S,T) c= Funcs the carrier of S,the carrier of T
UPS S,T is SubRelStr of T |^ the carrier of S by Def4;
then the carrier of (UPS S,T) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
hence the carrier of (UPS S,T) c= Funcs the carrier of S,the carrier of T by YELLOW_1:28; :: thesis: verum