We have the definitions
and
If we are willing to be slightly tricky, we can write more compactly
but then the proof might be more difficult for a computer program.
Next we have.
Theorem:
Up to this point, there is no creativity. Someone might argue that the decision to use set theory is creative, but I'm striving for a technical notion of creative solution, and one has to start with some background language. Taking set theory as background is more likely to lead to technical results than trying to use English.
The proofs are as follows: