theorem Th58: :: ZF_LANG:58

for F, H being ZF-formula st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )