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