Added the definition for "set builder", i.e., the image of a set s under some function f: { f(x) | x in s }. I consider this as a necessity for the set theory. The "set builder" is defined by a "set-induction" rewrite rule. Also added and proved properties for it.