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