let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for F, G being NAT -defined non empty FinPartState of st F c= G holds
FirstLoc G <= FirstLoc F,S
let S be non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N; :: thesis: for F, G being NAT -defined non empty FinPartState of st F c= G holds
FirstLoc G <= FirstLoc F,S
let F, G be NAT -defined non empty FinPartState of ; :: thesis: ( F c= G implies FirstLoc G <= FirstLoc F,S )
assume A1: F c= G ; :: thesis: FirstLoc G <= FirstLoc F,S
consider N being non empty Subset of NAT such that
A2: N = { (locnum l,S) where l is Element of NAT : l in dom G } and
A3: FirstLoc G = il. S,(min N) by Def2;
consider M being non empty Subset of NAT such that
A4: M = { (locnum l,S) where l is Element of NAT : l in dom F } and
A5: FirstLoc F = il. S,(min M) by Def2;
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 A6: ex l being Element of NAT st
( a = locnum l,S & l in dom F ) by A4;
dom F c= dom G by A1, GRFUNC_1:8;
hence a in N by A2, A6; :: thesis: verum

end;

then min N <= min M by XXREAL_2:60;
hence FirstLoc G <= FirstLoc F,S by A5, A3, AMISTD_1:28; :: thesis: verum