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

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