theorem Th2: :: AMI_5:2

for dl being Data-Location holds dl <> IC by Th1, AMI_3:13;