theorem :: QC_LANG2:44

for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_immediate_constituent_of FALSUM A iff H = VERUM A ) by Th43;