let Q be Element of untn P; :: thesis: Q is consistent
assume not Q is consistent ; :: thesis: contradiction
then A1: {} LTLB_WFF |- 'X' ('not' (Q ^)) by LTLAXIO1:44;
{} LTLB_WFF |- (P ^) => ('X' (Q ^)) by Th18;
then A2: {} LTLB_WFF |- ('not' ('X' (Q ^))) => ('not' (P ^)) by LTLAXIO1:52;
('X' ('not' (Q ^))) => ('not' ('X' (Q ^))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- ('X' ('not' (Q ^))) => ('not' ('X' (Q ^))) by LTLAXIO1:42;
then {} LTLB_WFF |- 'not' ('X' (Q ^)) by A1, LTLAXIO1:43;
hence contradiction by A2, LTLAXIO1:43, LTLAXIO3:def 10; :: thesis: verum