theorem Th50: :: QC_LANG2:50

for A being QC-alphabet
for F, H being Element of QC-WFF A st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )