let H be Element of QC-WFF ; :: thesis: not H is_immediate_constituent_of VERUM

A1: now

given H1 being Element of QC-WFF such that A2: ( VERUM = H '&' H1 or VERUM = H1 '&' H ) ; :: thesis: contradiction
( H '&' H1 is conjunctive & H1 '&' H is conjunctive ) by QC_LANG1:def 19;
hence contradiction by A2, QC_LANG1:49; :: thesis: verum

end;

'not' H is negative by QC_LANG1:def 18;
then A3: ((@ ('not' H)) . 1) `1 = 1 by QC_LANG1:49;
assume H is_immediate_constituent_of VERUM ; :: thesis: contradiction
then consider z being bound_QC-variable such that
A4: VERUM = All (z,H) by A3, A1, Def20, QC_LANG1:49;
All (z,H) is universal by QC_LANG1:def 20;
hence contradiction by A4, QC_LANG1:49; :: thesis: verum