let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N holds T is InsLoc-antisymmetric
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; :: thesis: T is InsLoc-antisymmetric
let l1, l2 be Element of NAT ; :: according to AMI_WSTD:def 2 :: thesis: ( l1 <= l2,T & l2 <= l1,T implies l1 = l2 )
assume A1: ( l1 <= l2,T & l2 <= l1,T ) ; :: thesis: l1 = l2
reconsider T = T as non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N ;
reconsider l1 = l1, l2 = l2 as Element of NAT ;
( locnum (l1,T) <= locnum (l2,T) & locnum (l2,T) <= locnum (l1,T) ) by A1, Th9;
hence l1 = l2 by Th7, XXREAL_0:1; :: thesis: verum