:: deftheorem defines atomic ZF_LANG:def 15 :
for H being ZF-formula holds
( H is atomic iff ( H is being_equality or H is being_membership ) );