:: deftheorem Def10 defines Inconsistent LTLAXIO3:def 10 :
for P being PNPair holds
( P is Inconsistent iff {} LTLB_WFF |- 'not' (P ^) );