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