theorem Th44: :: ZF_LANG:44

for H being ZF-formula st H is universal holds
H = All ((bound_in H),(the_scope_of H))