set u = { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y' } ;
A1: { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y' } c= I

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y' } or x in I )
assume x in { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y' } ; :: thesis: x in I
then consider x'' being Element of I such that
A2: ( x'' = x & ( for x', y' being Polynomial of L st x' = x'' & y' in I holds
len x' <= len y' ) ) ;
thus x in I by A2; :: thesis: verum

end;

defpred S₁[ Element of I, Element of NAT ] means for p being Polynomial of L st $1 = p holds
$2 = len p;

A3: now

let x be Element of I; :: thesis: ex y being Element of NAT st S₁[x,y]
reconsider x' = x as Polynomial of L by POLYNOM3:def 12;
for p being Polynomial of L st x = p holds
len x' = len p ;
hence ex y being Element of NAT st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of I,NAT such that
A4: for x being Element of I holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
I c= I ;
then reconsider I' = I as non empty Subset of I ;
min (f .: I') in f .: I by XXREAL_2:def 7;
then consider x being set such that
A5: ( x in dom f & x in I & min (f .: I') = f . x ) by FUNCT_1:def 12;
reconsider x = x as Element of I by A5;

now

let x', y' be Polynomial of L; :: thesis: ( x' = x & y' in I implies len x' <= len y' )
assume A6: ( x' = x & y' in I ) ; :: thesis: len x' <= len y'
dom f = I by FUNCT_2:def 1;
then f . y' in f .: I by A6, FUNCT_1:def 12;
then f . x <= f . y' by A5, XXREAL_2:def 7;
then len x' <= f . y' by A4, A6;
hence len x' <= len y' by A4, A6; :: thesis: verum

end;

then x in { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y' } ;
hence { x where x is Element of I : for x', y' being Polynomial of L st x' = x & y' in I holds
len x' <= len y' } is non empty Subset of I by A1; :: thesis: verum