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 ((Omega Y) |^ the carrier of X) by XBOOLE_1:1;

pi (A,x) is Subset of (Omega Y) ;

hence pi (A,x) is Subset of (Omega Y) ; :: thesis: verum

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 ((Omega Y) |^ the carrier of X) by XBOOLE_1:1;

pi (A,x) is Subset of (Omega Y) ;

hence pi (A,x) is Subset of (Omega Y) ; :: thesis: verum