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

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

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

end;

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