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 Th2, Th6;
hence 0 in k -SD_Sub ; :: thesis: verum