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

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

let x be set ; :: thesis: ( x in LocNums F,S implies x in {n} )
assume x in LocNums F,S ; :: thesis: x in {n}
then consider l being Element of NAT such that
A3: x = locnum l,S 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,S )
assume x in {n} ; :: thesis: x in LocNums F,S
then x = n by TARSKI:def 1;
hence x in LocNums F,S by A2, A1; :: thesis: verum