let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for F being NAT -defined non empty FinPartState of
for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
let T be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N; :: thesis: for F being NAT -defined non empty FinPartState of
for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
let F be NAT -defined non empty FinPartState of ; :: thesis: for l being Element of NAT st l in dom F holds
l <= LastLoc F,T
let l be Element of NAT ; :: thesis: ( l in dom F implies l <= LastLoc F,T )
assume A1: l in dom F ; :: thesis: l <= LastLoc F,T
consider M being non empty finite natural-membered set such that
A2: M = { (locnum (w,T)) where w is Element of NAT : w in dom F } and
A3: LastLoc F = il. (T,(max M)) by Def21;
locnum (l,T) in M by A1, A2;
then A4: locnum (l,T) <= max M by XXREAL_2:def 8;
locnum ((LastLoc F),T) = max M by A3, Def13;
hence l <= LastLoc F,T by A4, Th29; :: thesis: verum