(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