for l3 being Element of NAT
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for l1, l2 being Nat st l1 <= l2,S & l2 <= l3,S holds
l1 <= l3,S