theorem :: ZF_FUND1:23

for V being Universe
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
( n in X & 0-element_of V in X & 1-element_of V in X ) by Lm12, Lm13;