deffunc H₁( Element of NAT ) -> Element of NAT = R;
for k being Nat holds
( k + 1 in SUCC (k,(SCM R)) & ( for j being Nat st j in SUCC (k,(SCM R)) holds
k <= j ) ) by Th35;
hence SCM R is standard by AMISTD_1:3; :: thesis: verum