let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over 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 with_non-empty_values IC-Ins-separated Mem-Struct over 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 in dom p by Def11;
A2: IC p = l by Def11;
let s be PartState of S; :: thesis: ( p c= s implies s is l -started )
assume A3: p c= s ; :: thesis: s is l -started
then dom p c= dom s by RELAT_1:11;
hence IC in dom s by A1; :: according to MEMSTR_0:def 11 :: thesis: IC s = l
thus IC s = l by A3, A2, A1, GRFUNC_1:2; :: thesis: verum