let a, b be Real; :: thesis: ( a < b implies <*a,b*> is non empty increasing FinSequence of REAL )
assume A1: a < b ; :: thesis: <*a,b*> is non empty increasing FinSequence of REAL
set s = <*a,b*>;
A2: rng <*a,b*> c= REAL ;
<*a,b*> is increasing

proof

now :: thesis: for e1, e2 being ExtReal st e1 in dom <*a,b*> & e2 in dom <*a,b*> & e1 < e2 holds
<*a,b*> . e1 < <*a,b*> . e2

let e1, e2 be ExtReal; :: thesis: ( e1 in dom <*a,b*> & e2 in dom <*a,b*> & e1 < e2 implies <*a,b*> . e1 < <*a,b*> . e2 )
assume that
A3: e1 in dom <*a,b*> and
A4: e2 in dom <*a,b*> and
A5: e1 < e2 ; :: thesis: <*a,b*> . e1 < <*a,b*> . e2
dom <*a,b*> = Seg (len <*a,b*>) by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44 ;
then ( ( e1 = 1 or e1 = 2 ) & ( e2 = 1 or e2 = 2 ) ) by TARSKI:def 2, A3, A4, FINSEQ_1:2;
then ( <*a,b*> . e1 = a & <*a,b*> . e2 = b ) by A5;
hence <*a,b*> . e1 < <*a,b*> . e2 by A1; :: thesis: verum

end;

hence <*a,b*> is increasing ; :: thesis: verum

end;

hence <*a,b*> is non empty increasing FinSequence of REAL by A2, FINSEQ_1:def 4; :: thesis: verum