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