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