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