let dl be Int_position ; :: thesis: dl <> IC
ObjectKind dl = INT by Th13;
hence dl <> IC by MEMSTR_0:def 3, NUMBERS:27; :: thesis: verum