let a be Int_position ; :: thesis: for k1 being Integer
for I, J being Program of SCMPDS holds
( inspos 0 in dom (if>0 a,k1,I,J) & inspos 1 in dom (if>0 a,k1,I,J) )
let k1 be Integer; :: thesis: for I, J being Program of SCMPDS holds
( inspos 0 in dom (if>0 a,k1,I,J) & inspos 1 in dom (if>0 a,k1,I,J) )
let I, J be Program of SCMPDS ; :: thesis: ( inspos 0 in dom (if>0 a,k1,I,J) & inspos 1 in dom (if>0 a,k1,I,J) )
set ci = card (if>0 a,k1,I,J);
card (if>0 a,k1,I,J) = ((card I) + (card J)) + 2 by Lm4;
then 2 <= card (if>0 a,k1,I,J) by NAT_1:12;
then ( 0 < card (if>0 a,k1,I,J) & 1 < card (if>0 a,k1,I,J) ) by XXREAL_0:2;
hence ( inspos 0 in dom (if>0 a,k1,I,J) & inspos 1 in dom (if>0 a,k1,I,J) ) by SCMPDS_4:1; :: thesis: verum