let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for I being non empty Subset of (Polynom-Ring L)

for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds

( i1 in I & len i1 <= len i2 )

let I be non empty Subset of (Polynom-Ring L); :: thesis: for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds

( i1 in I & len i1 <= len i2 )

let i1, i2 be Polynomial of L; :: thesis: ( i1 in minlen I & i2 in I implies ( i1 in I & len i1 <= len i2 ) )

assume that

A1: i1 in minlen I and

A2: i2 in I ; :: thesis: ( i1 in I & len i1 <= len i2 )

ex i19 being Element of I st

( i19 = i1 & ( for x9, y9 being Polynomial of L st x9 = i19 & y9 in I holds

len x9 <= len y9 ) ) by A1;

hence ( i1 in I & len i1 <= len i2 ) by A2; :: thesis: verum

for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds

( i1 in I & len i1 <= len i2 )

let I be non empty Subset of (Polynom-Ring L); :: thesis: for i1, i2 being Polynomial of L st i1 in minlen I & i2 in I holds

( i1 in I & len i1 <= len i2 )

let i1, i2 be Polynomial of L; :: thesis: ( i1 in minlen I & i2 in I implies ( i1 in I & len i1 <= len i2 ) )

assume that

A1: i1 in minlen I and

A2: i2 in I ; :: thesis: ( i1 in I & len i1 <= len i2 )

ex i19 being Element of I st

( i19 = i1 & ( for x9, y9 being Polynomial of L st x9 = i19 & y9 in I holds

len x9 <= len y9 ) ) by A1;

hence ( i1 in I & len i1 <= len i2 ) by A2; :: thesis: verum