let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F, G being non empty programmed FinPartState of T st F c= G holds
LastLoc F <= LastLoc G
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F, G being non empty programmed FinPartState of T st F c= G holds
LastLoc F <= LastLoc G
let F, G be non empty programmed FinPartState of T; :: thesis: ( F c= G implies LastLoc F <= LastLoc G )
assume A1: F c= G ; :: thesis: LastLoc F <= LastLoc G
consider M being non empty finite natural-membered set such that
A2: M = { (locnum l) where l is Instruction-Location of T : l in dom F } and
A3: LastLoc F = il. T,(max M) by Def21;
consider N being non empty finite natural-membered set such that
A4: N = { (locnum l) where l is Instruction-Location of T : l in dom G } and
A5: LastLoc G = il. T,(max N) by Def21;
reconsider MM = M, NN = N as non empty finite Subset of REAL by MEMBERED:3;
M c= N

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in M or a in N )
assume a in M ; :: thesis: a in N
then consider l being Instruction-Location of T such that
A6: ( a = locnum l & l in dom F ) by A2;
dom F c= dom G by A1, GRFUNC_1:8;
hence a in N by A4, A6; :: thesis: verum

end;

then max MM <= max NN by XXREAL_2:59;
hence LastLoc F <= LastLoc G by A3, A5, Th28; :: thesis: verum