let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A holds not H is_immediate_constituent_of VERUM A
let H be Element of QC-WFF A; :: thesis: not H is_immediate_constituent_of VERUM A
( not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal ) by QC_LANG1:20;
then ( not VERUM A = 'not' H & ( for H1 being Element of QC-WFF A holds
( not VERUM A = H '&' H1 & not VERUM A = H1 '&' H ) ) & ( for x being bound_QC-variable of A holds not VERUM A = All (x,H) ) ) ;
hence not H is_immediate_constituent_of VERUM A ; :: thesis: verum