theorem Th29: :: LTLAXIO3:29

for A being Element of LTLB_WFF
for P being PNPair st A in rng (P `2) holds
{} LTLB_WFF |- (P ^) => ('not' A)