theorem Th29: :: LTLAXIO4:29

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