let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite COM-Struct of N
for l being Nat
for p being b₂ -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
let S be non empty stored-program IC-Ins-separated definite COM-Struct of N; :: thesis: for l being Nat
for p being b₁ -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
let l be Nat; :: thesis: for p being l -started PartState of S
for s being PartState of S st p c= s holds
s is l -started
let p be l -started PartState of S; :: thesis: for s being PartState of S st p c= s holds
s is l -started
A1: IC S in dom p by Def41;
A2: IC p = l by Def41;
let s be PartState of S; :: thesis: ( p c= s implies s is l -started )
assume Z: p c= s ; :: thesis: s is l -started
then dom p c= dom s by RELAT_1:25;
hence IC S in dom s by A1; :: according to COMPOS_1:def 16 :: thesis: IC s = l
thus IC s = l by Z, A2, A1, GRFUNC_1:8; :: thesis: verum