theorem Th31: :: LTLAXIO3:31

for A being Element of LTLB_WFF
for P being consistent PNPair holds
( A in rng P or [((P `1) ^^ <*A*>),(P `2)] is consistent or [(P `1),((P `2) ^^ <*A*>)] is consistent )