>>299 Sorry, I haven't seen that notation for the last equation before, is that supposed to be axiom of infinity? Does y' represent successor? I've seen {y} U y and S(y).