let i, j be Instruction of ; :: thesis: for I being Program of holds
( inspos 0 in dom ((i ';' j) ';' I) & inspos 1 in dom ((i ';' j) ';' I) )
let I be Program of ; :: thesis: ( inspos 0 in dom ((i ';' j) ';' I) & inspos 1 in dom ((i ';' j) ';' I) )
set ci = card ((i ';' j) ';' I);
card ((i ';' j) ';' I) = (card I) + 2 by Lm8;
then 2 <= card ((i ';' j) ';' I) by NAT_1:11;
then 1 < card ((i ';' j) ';' I) by XXREAL_0:2;
hence ( inspos 0 in dom ((i ';' j) ';' I) & inspos 1 in dom ((i ';' j) ';' I) ) by SCMPDS_4:1; :: thesis: verum