:: deftheorem defines the_axiom_of_infinity ZF_MODEL:def 9 :
the_axiom_of_infinity = Ex ((x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))));