:: deftheorem defines universal ZF_LANG:def 14 :
for H being ZF-formula holds
( H is universal iff ex x being Variable ex H1 being ZF-formula st H = All (x,H1) );