if>0 (a,b,I,J) = (SubFrom (a,b)) ";" (if>0 (a,I,J)) by SCMFSA8B:def 5;
hence if>0 (a,b,I,J) is good ; :: thesis: verum