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