:: deftheorem defines closed_wrt_A1 ZF_FUND1:def 6 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A1 iff for a being Element of V st a in X holds
{ {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a ) } in X );