theorem :: COUSIN:48

for s1, s2 being non empty increasing FinSequence of REAL
for r being Real st s1 . (len s1) < r & r < s2 . 1 holds
(s1 ^ <*r*>) ^ s2 is non empty increasing FinSequence of REAL