let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for I being non empty Subset of
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 ; :: 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 i1' being Element of I st
( i1' = i1 & ( for x', y' being Polynomial of L st x' = i1' & y' in I holds
len x' <= len y' ) ) by A1;
hence ( i1 in I & len i1 <= len i2 ) by A2; :: thesis: verum