thus ( not VERUM is atomic & not VERUM is negative & not VERUM is conjunctive & not VERUM is universal ) by Th49, Th50; :: thesis: for p being Element of QC-WFF holds
( not ( p is atomic & p is negative ) & not ( p is atomic & p is conjunctive ) & not ( p is atomic & p is universal ) & not ( p is negative & p is conjunctive ) & not ( p is negative & p is universal ) & not ( p is conjunctive & p is universal ) )
let p be Element of QC-WFF ; :: thesis: ( not ( p is atomic & p is negative ) & not ( p is atomic & p is conjunctive ) & not ( p is atomic & p is universal ) & not ( p is negative & p is conjunctive ) & not ( p is negative & p is universal ) & not ( p is conjunctive & p is universal ) )
( ((@ VERUM ) . 1) `1 = 0 & ( p is negative implies ((@ p) . 1) `1 = 1 ) & ( p is conjunctive implies ((@ p) . 1) `1 = 2 ) & ( p is universal implies ((@ p) . 1) `1 = 3 ) ) by Th49;
hence ( not ( p is atomic & p is negative ) & not ( p is atomic & p is conjunctive ) & not ( p is atomic & p is universal ) & not ( p is negative & p is conjunctive ) & not ( p is negative & p is universal ) & not ( p is conjunctive & p is universal ) ) by Th50; :: thesis: verum