theorem Th17: :: LTLAXIO4:17

for P being consistent PNPair
for f being FinSequence of LTLB_WFF st rng f = (comp P) ^ holds
{} LTLB_WFF |- (P ^) => ('not' ((con (nega f)) /. (len (con (nega f)))))