let r1, r2, r3, r4 be Real; :: thesis: ( r1 < r2 & r2 < r3 & r3 < r4 implies <*r1,r2,r3,r4*> is increasing )
assume ( r1 < r2 & r2 < r3 ) ; :: thesis: ( not r3 < r4 or <*r1,r2,r3,r4*> is increasing )
then A1: <*r1,r2,r3*> is increasing by Th40;
A2: len <*r1,r2,r3*> = 3 by CARD_1:def 7;
( <*r1,r2,r3*> . 3 = r3 & <*r4*> . 1 = r4 ) ;
hence ( not r3 < r4 or <*r1,r2,r3,r4*> is increasing ) by A1, A2, Th38; :: thesis: verum