let dl be Int_position; :: thesis: dl <> IC
Values dl = INT by Th5;
hence dl <> IC by MEMSTR_0:def 6, NUMBERS:27; :: thesis: verum