:: deftheorem defines minlen HILBASIS:def 4 :
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) holds minlen I = { x where x is Element of I : for x9, y9 being Polynomial of L st x9 = x & y9 in I holds
len x9 <= len y9 } ;