let I be Program of SCMPDS ; :: thesis: for s being State of SCMPDS st not IC s in dom I holds
not succ (IC s) in dom I
let s be State of SCMPDS ; :: thesis: ( not IC s in dom I implies not succ (IC s) in dom I )
reconsider m = IC s as Element of NAT ;
assume not IC s in dom I ; :: thesis: not succ (IC s) in dom I
then A1: m >= card I by Th1;
m + 1 >= m by NAT_1:11;
then m + 1 >= card I by A1, XXREAL_0:2;
hence not succ (IC s) in dom I by Th1; :: thesis: verum