let P be PNPair; :: thesis: ( P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] implies not P is Inconsistent )
assume A1: P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] ; :: thesis: not P is Inconsistent
not {} LTLB_WFF |= 'not' (P ^)
proof
reconsider M = NAT --> {} as LTLModel by Th2;
set s = SAT M;
take M ; :: according to LTLAXIO1:def 14 :: thesis: ( M |= {} LTLB_WFF & not M |= 'not' (P ^) )
thus M |= {} LTLB_WFF ; :: thesis: not M |= 'not' (P ^)
(SAT M) . [0,('not' (P ^))] <> 1
proof
assume (SAT M) . [0,('not' (P ^))] = 1 ; :: thesis: contradiction
then (SAT M) . [0,(P ^)] = 0 by LTLAXIO1:5;
then (SAT M) . [0,TVERUM] <> 1 by LTLAXIO1:7, A1, Th27;
hence contradiction by LTLAXIO1:6; :: thesis: verum
end;
hence not M |= 'not' (P ^) ; :: thesis: verum
end;
hence P is consistent by LTLAXIO1:41; :: thesis: verum