:: deftheorem defines being_membership ZF_LANG:def 11 :
for H being ZF-formula holds
( H is being_membership iff ex x, y being Variable st H = x 'in' y );