theorem Th16: :: LTLAXIO4:16

for F being finite Subset of LTLB_WFF
for f being FinSequence of LTLB_WFF st rng f = (comp F) ^ holds
{} LTLB_WFF |- 'not' ((con (nega f)) /. (len (con (nega f))))