set b = the Element of S;
consider IT being Function of NAT,S such that
IT . 0 = the Element of S 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