:: deftheorem Def29 defines Var2 ZF_LANG:def 29 :
for H being ZF-formula st H is atomic holds
Var2 H = H . 3;