let k be Nat; :: thesis: 0 in k -SD_Sub
A1: 0 in k -SD_Sub_S by Th7;
k -SD_Sub_S c= k -SD_Sub by Th3;
hence 0 in k -SD_Sub by A1; :: thesis: verum