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