theorem Th12: :: ZF_FUND1:12

for V being Universe
for a, b being Element of V
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & b in X holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X