let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of T holds
( locnum l1 <= locnum l2 iff l1 <= l2 )
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l1, l2 being Instruction-Location of T holds
( locnum l1 <= locnum l2 iff l1 <= l2 )
let l1, l2 be Instruction-Location of T; :: thesis: ( locnum l1 <= locnum l2 iff l1 <= l2 )
( il. T,(locnum l1) = l1 & il. T,(locnum l2) = l2 ) by Def13;
hence ( locnum l1 <= locnum l2 iff l1 <= l2 ) by Th28; :: thesis: verum