theorem :: ZF_FUND1:30

for A being Element of omega holds A = x". (x. (card A)) by Lm2;