let k be Nat; :: thesis: k -SD_Sub c= INT

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub or e in INT )

assume e in k -SD_Sub ; :: thesis: e in INT

then e is Integer by Th8;

hence e in INT by INT_1:def 2; :: thesis: verum

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD_Sub or e in INT )

assume e in k -SD_Sub ; :: thesis: e in INT

then e is Integer by Th8;

hence e in INT by INT_1:def 2; :: thesis: verum