consider b being Element of S;
consider IT being Function of NAT,S such that
IT . 0 = b and
A1: for n being Element of NAT holds [(IT . n),(IT . (n + 1))] in R by Lm34;
take IT ; :: thesis: for n being Element of NAT holds [(IT . n),(IT . (n + 1))] in R
thus for n being Element of NAT holds [(IT . n),(IT . (n + 1))] in R by A1; :: thesis: verum