Manuscript IX-E@1 · IX-E.tex · section · 8f8d5e7f
E6: conditional unnormalized subtraction
E6: conditional unnormalized subtraction · lines 981–985
The next result audits directly the binary implication quoted from IX-D. It does not presume that its hypotheses have been discharged.