let P be consistent PNPair; :: thesis: not TFALSUM in rng (P `1)
assume TFALSUM in rng (P `1) ; :: thesis: contradiction
then {} LTLB_WFF |- 'not' (P ^) by Th28;
hence contradiction by Def10; :: thesis: verum