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 A1: ( i1 in minlen I & i2 in I ) ; :: thesis: ( i1 in I & len i1 <= len i2 )
then consider i1' being Element of I such that
A2: ( i1' = i1 & ( for x', y' being Polynomial of L st x' = i1' & y' in I holds
len x' <= len y' ) ) ;
thus ( i1 in I & len i1 <= len i2 ) by A1, A2; :: thesis: verum