let k be Nat; :: thesis: 0 in k -SD_Sub_S
defpred S₁[ Nat] means 0 in $1 -SD_Sub_S ;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let kk be Nat; :: thesis: ( S₁[kk] implies S₁[kk + 1] )
assume A2: 0 in kk -SD_Sub_S ; :: thesis: S₁[kk + 1]
kk -SD_Sub_S c= (kk + 1) -SD_Sub_S by Th3;
hence S₁[kk + 1] by A2; :: thesis: verum

end;

A3: S₁[ 0 ] by Th5;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence 0 in k -SD_Sub_S ; :: thesis: verum