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} )
A1: ( il. S,n in {(il. S,n)} & locnum (il. S,n) = n ) by AMISTD_1:def 13, TARSKI:def 1;
assume A2: F = {(il. S,n)} ; :: thesis: LocNums F = {n}

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
A3: x = locnum l and
A4: l in F ;
l = il. S,n by A2, A4, TARSKI:def 1;
then x = n by A3, 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 A2, A1; :: thesis: verum