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