let k be Nat; :: thesis: k -SD_Sub_S c= INT
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub_S or e in INT )
assume A1: e in k -SD_Sub_S ; :: thesis: e in INT
k -SD_Sub_S c= k -SD_Sub by Th2;
then e is Integer by A1, Th8;
hence e in INT by INT_1:def 2; :: thesis: verum