theorem :: LTLAXIO3:32

for P being consistent PNPair holds not TFALSUM in rng (P `1)