let r1, r2, r3 be Real; :: thesis: ( r1 < r2 & r2 < r3 implies <*r1,r2,r3*> is increasing )
assume r1 < r2 ; :: thesis: ( not r2 < r3 or <*r1,r2,r3*> is increasing )
then A1: <*r1,r2*> is increasing by Th39;
A2: len <*r1,r2*> = 2 by FINSEQ_1:44;
( <*r1,r2*> . 2 = r2 & <*r3*> . 1 = r3 ) ;
hence ( not r2 < r3 or <*r1,r2,r3*> is increasing ) by A1, A2, Th38; :: thesis: verum