defpred S₁[ set ] means ex g being natural-valued ManySortedSet of X st
( $1 = g & ( for x being set st x in X holds
g . x <= f . x ) );
consider IT being Subset of (Funcs X,NAT ) such that
A1: for h being set holds
( h in IT iff ( h in Funcs X,NAT & S₁[h] ) ) from SUBSET_1:sch 1();
take IT ; :: thesis: for g being natural-valued ManySortedSet of X holds
( g in IT iff for x being set st x in X holds
g . x <= f . x )
let g be natural-valued ManySortedSet of X; :: thesis: ( g in IT iff for x being set st x in X holds
g . x <= f . x )

hereby :: thesis: ( ( for x being set st x in X holds
g . x <= f . x ) implies g in IT )

assume g in IT ; :: thesis: for x being set st x in X holds
g . x <= f . x
then consider g1 being natural-valued ManySortedSet of X such that
A2: ( g1 = g & ( for x being set st x in X holds
g1 . x <= f . x ) ) by A1;
thus for x being set st x in X holds
g . x <= f . x by A2; :: thesis: verum

end;

assume A3: for x being set st x in X holds
g . x <= f . x ; :: thesis: g in IT
( dom g = X & rng g c= NAT ) by PBOOLE:def 3, VALUED_0:def 6;
then g is Function of X, NAT by FUNCT_2:def 1, RELSET_1:11;
then g in Funcs X,NAT by FUNCT_2:11;
hence g in IT by A1, A3; :: thesis: verum