:: deftheorem Def28 defines Var1 ZF_LANG:def 28 :
for H being ZF-formula st H is atomic holds
Var1 H = H . 2;