theorem :: ZF_LANG:88

for H being ZF-formula st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}