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 l1 being Instruction-Location of S
for F being IL-Subset of S holds
( locnum l1 in LocNums F iff l1 in F )
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l1 being Instruction-Location of S
for F being IL-Subset of S holds
( locnum l1 in LocNums F iff l1 in F )
let l1 be Instruction-Location of S; :: thesis: for F being IL-Subset of S holds
( locnum l1 in LocNums F iff l1 in F )
let F be IL-Subset of S; :: thesis: ( locnum l1 in LocNums F iff l1 in F )

hereby :: thesis: ( l1 in F implies locnum l1 in LocNums F )

assume locnum l1 in LocNums F ; :: thesis: l1 in F
then ex l being Instruction-Location of S st
( locnum l1 = locnum l & l in F ) ;
hence l1 in F by AMISTD_1:27; :: thesis: verum

end;

thus ( l1 in F implies locnum l1 in LocNums F ) ; :: thesis: verum