theorem Th3: :: SCMPDS_4:3
for k1, k2 being Nat st k1 <> k2 holds
DataLoc (k1,0) <> DataLoc (k2,0)