let a be PNPair; :: thesis: ( a = [(P `1),(P `2)] implies not a is Inconsistent )
assume a = [(P `1),(P `2)] ; :: thesis: not a is Inconsistent
then A1: ( a `1 = P `1 & a `2 = P `2 ) ;
not {} LTLB_WFF |- 'not' (P ^) by Def10;
then not {} LTLB_WFF |- 'not' (a ^) by A1;
hence a is consistent ; :: thesis: verum