set XY = oContMaps X,Y;
oContMaps X,Y is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;
then the carrier of (oContMaps X,Y) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def 13;
then reconsider A = A as Subset of by XBOOLE_1:1;
pi A,x is Subset of ;
hence pi A,x is Subset of ; :: thesis: verum