let a be Int_position; for k1 being Integer
for I, J being Program of holds
( 0 in dom (if>0 (a,k1,I,J)) & 1 in dom (if>0 (a,k1,I,J)) )
let k1 be Integer; for I, J being Program of holds
( 0 in dom (if>0 (a,k1,I,J)) & 1 in dom (if>0 (a,k1,I,J)) )
let I, J be Program of ; ( 0 in dom (if>0 (a,k1,I,J)) & 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
1 < card (if>0 (a,k1,I,J))
by XXREAL_0:2;
hence
( 0 in dom (if>0 (a,k1,I,J)) & 1 in dom (if>0 (a,k1,I,J)) )
by AFINSQ_1:66; verum