let A be QC-alphabet ; :: thesis: ( not VERUM A is atomic & not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal & ( for p being Element of QC-WFF A 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 ) ) ) )
((@ (VERUM A)) . 1) `1 = 0 ;
hence ( not VERUM A is atomic & not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal ) by Th18, Th19; :: thesis: for p being Element of QC-WFF A 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 A; :: 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 Th18;
A2: ( p is universal implies ((@ p) . 1) `1 = 3 ) by Th18;
( p is negative implies ((@ p) . 1) `1 = 1 ) by Th18;
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, Th19; :: thesis: verum