theorem :: LTLAXIO3:33

for A, B being Element of LTLB_WFF
for P being consistent PNPair st A in rng P & B in rng P & A => B in rng P holds
( A => B in rng (P `1) iff ( A in rng (P `2) or B in rng (P `1) ) )