I c= I ;
then reconsider I9 = I as non empty Subset of I ;
defpred S₁[ Element of I, Element of NAT ] means for p being Polynomial of L st $1 = p holds
$2 = len p;
set u = { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;

A1: now :: thesis: for x being Element of I ex y being Element of NAT st S₁[x,y]

let x be Element of I; :: thesis: ex y being Element of NAT st S₁[x,y]
reconsider x9 = x as Polynomial of L by POLYNOM3:def 10;
for p being Polynomial of L st x = p holds
len x9 = 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
A2: for x being Element of I holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
min (f .: I9) in f .: I by XXREAL_2:def 7;
then consider x being object such that
A3: x in dom f and
x in I and
A4: min (f .: I9) = f . x by FUNCT_1:def 6;
reconsider x = x as Element of I by A3;

now :: thesis: for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9

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

end;

then A7: x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;
{ x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } c= I

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } or x in I )
assume x in { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ; :: thesis: x in I
then ex x99 being Element of I st
( x99 = x & ( for x9, y9 being Polynomial of L st x9 = x99 & y9 in I holds
len x9 <= len y9 ) ) ;
hence x in I ; :: thesis: verum

end;

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