theorem :: ZF_LANG:75

for H being ZF-formula st H is universal holds
the_scope_of H is_proper_subformula_of H