theorem Th17: :: HILBASIS:17

for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
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 )