theorem Th17: :: ZF_FUND1:17

for V being Universe
for a being Element of V
for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X