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 ) )
A1: ( p is conjunctive implies ((@ p) . 1) `1 = 2 ) by Th49;
A2: ( p is universal implies ((@ p) . 1) `1 = 3 ) by Th49;
( p is negative implies ((@ p) . 1) `1 = 1 ) 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 A1, A2, Th50; :: thesis: verum