let A be QC-alphabet ; :: thesis: for S being Element of QC-Sub-WFF A holds
( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )
let S be Element of QC-Sub-WFF A; :: thesis: ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) )
A1: ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) by Th25;
A2: ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) by Th25;
A3: ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) by Th25;
( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) by Th25;
hence ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) ) by A1, A2, A3, Th26; :: thesis: verum