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 holds T is InsLoc-antisymmetric
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: T is InsLoc-antisymmetric
let l1, l2 be Instruction-Location of T; :: according to AMISTD_1:def 9 :: thesis: ( l1 <= l2 & l2 <= l1 implies l1 = l2 )
assume A1: ( l1 <= l2 & l2 <= l1 ) ; :: thesis: l1 = l2
reconsider T = T as non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N ;
reconsider l1 = l1, l2 = l2 as Instruction-Location of T ;
( locnum l1 <= locnum l2 & locnum l2 <= locnum l1 ) by A1, Th29;
hence l1 = l2 by Th27, XXREAL_0:1; :: thesis: verum