let k be Nat; :: thesis: k -SD c= INT
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in k -SD or e in INT )
assume e in k -SD ; :: thesis: e in INT
then e is Integer by Th13;
hence e in INT by INT_1:def 2; :: thesis: verum