:: deftheorem defines '=' ZF_LANG:def 3 :
for x, y being Variable holds x '=' y = (<*0*> ^ <*x*>) ^ <*y*>;