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