theorem :: LTLAXIO3:30

for P being consistent PNPair holds rng (P `1) misses rng (P `2)