[see also: superfluous, unnecessary, drop, omit
Note that no boundedness assumption is made in this definition; in fact, this would be redundant as shown by Theorem 3 below.