let n be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being IL-Subset of S st F = {(il. S,n)} holds
LocNums F = {n}
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being IL-Subset of S st F = {(il. S,n)} holds
LocNums F = {n}
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being IL-Subset of S st F = {(il. S,n)} holds
LocNums F = {n}
let F be IL-Subset of S; :: thesis: ( F = {(il. S,n)} implies LocNums F = {n} )
assume A1: F = {(il. S,n)} ; :: thesis: LocNums F = {n}
A2: il. S,n in {(il. S,n)} by TARSKI:def 1;
A3: locnum (il. S,n) = n by AMISTD_1:def 13;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {n} c= LocNums F

let x be set ; :: thesis: ( x in LocNums F implies x in {n} )
assume x in LocNums F ; :: thesis: x in {n}
then consider l being Instruction-Location of S such that
A4: x = locnum l and
A5: l in F ;
l = il. S,n by A1, A5, TARSKI:def 1;
then x = n by A4, AMISTD_1:def 13;
hence x in {n} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {n} or x in LocNums F )
assume x in {n} ; :: thesis: x in LocNums F
then x = n by TARSKI:def 1;
hence x in LocNums F by A1, A2, A3; :: thesis: verum