let il be Element of NAT ; :: thesis: for dl being Data-Location holds il <> dl
let dl be Data-Location; :: thesis: il <> dl
ex j being Element of NAT st dl = dl. j by Th1;
hence il <> dl ; :: thesis: verum