let k be Nat; :: thesis: 0 in k -SD_Sub
( 0 in k -SD_Sub_S & k -SD_Sub_S c= k -SD_Sub ) by Th3, Th7;
hence 0 in k -SD_Sub ; :: thesis: verum