let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for p being FinPartState of S
for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for p being FinPartState of S
for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let p be FinPartState of S; :: thesis: for l being Element of NAT st p starts_at l holds
for s being State of S st p c= s holds
s starts_at l
let l be Element of NAT ; :: thesis: ( p starts_at l implies for s being State of S st p c= s holds
s starts_at l )
assume that
A1: IC S in dom p and
A2: IC p = l ; :: according to AMI_1:def 44 :: thesis: for s being State of S st p c= s holds
s starts_at l
let s be State of S; :: thesis: ( p c= s implies s starts_at l )
assume p c= s ; :: thesis: s starts_at l
hence IC s = l by A2, A1, GRFUNC_1:8; :: according to AMI_1:def 41 :: thesis: verum