let a be Int_position ; :: thesis: for i being Integer
for I being Program of SCMPDS holds
( inspos 0 in dom (while<>0 a,i,I) & inspos 1 in dom (while<>0 a,i,I) )
let i be Integer; :: thesis: for I being Program of SCMPDS holds
( inspos 0 in dom (while<>0 a,i,I) & inspos 1 in dom (while<>0 a,i,I) )
let I be Program of SCMPDS ; :: thesis: ( inspos 0 in dom (while<>0 a,i,I) & inspos 1 in dom (while<>0 a,i,I) )
A1: 3 <= (card I) + 3 by NAT_1:11;
then A2: 0 < (card I) + 3 by XXREAL_0:2;
1 < (card I) + 3 by A1, XXREAL_0:2;
hence ( inspos 0 in dom (while<>0 a,i,I) & inspos 1 in dom (while<>0 a,i,I) ) by A2, Th13; :: thesis: verum