let k be Nat; :: thesis: 0 in k -SD_Sub_S

defpred S_{1}[ Nat] means 0 in $1 -SD_Sub_S ;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Th5;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A3, A1);

hence 0 in k -SD_Sub_S ; :: thesis: verum

defpred S

A1: for k being Nat st S

S

proof

A3:
S
let kk be Nat; :: thesis: ( S_{1}[kk] implies S_{1}[kk + 1] )

assume A2: 0 in kk -SD_Sub_S ; :: thesis: S_{1}[kk + 1]

kk -SD_Sub_S c= (kk + 1) -SD_Sub_S by Th3;

hence S_{1}[kk + 1]
by A2; :: thesis: verum

end;assume A2: 0 in kk -SD_Sub_S ; :: thesis: S

kk -SD_Sub_S c= (kk + 1) -SD_Sub_S by Th3;

hence S

for k being Nat holds S

hence 0 in k -SD_Sub_S ; :: thesis: verum