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