I c= I ;
then reconsider I9 = I as non empty Subset of I ;
defpred S1[ 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 S1[x,y]
let x be Element of I; :: thesis: ex y being Element of NAT st S1[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 S1[x,y] ; :: thesis: verum
end;
consider f being Function of I,NAT such that
A2: for x being Element of I holds S1[x,f . x] from 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 ;
then f . x <= f . y9 by ;
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