(Support p) \ (Upper_Support (p,T,i)) c= Support p by XBOOLE_1:36;
hence (Support p) \ (Upper_Support (p,T,i)) is finite Subset of (Bags n) by XBOOLE_1:1; :: thesis: verum