:: deftheorem defines closed_wrt_A4 ZF_FUND1:def 9 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A4 iff for a, b being Element of V st a in X & b in X holds
{ {[x,y]} where x, y is Element of V : ( x in a & y in b ) } in X );