let a, b, c, d be Real; :: thesis: for f being Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d) st a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d holds
for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
let f be Function of (Closed-Interval-TSpace a,b),(Closed-Interval-TSpace c,d); :: thesis: ( a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d implies for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy )
assume A1: ( a < b & c < d & f is continuous & f is one-to-one & f . a = c & f . b = d ) ; :: thesis: for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
then A2: [.a,b.] = the carrier of (Closed-Interval-TSpace a,b) by TOPMETR:25;
A3: dom f = the carrier of (Closed-Interval-TSpace a,b) by FUNCT_2:def 1;
A4: [.a,b.] /\ (dom f) = [.a,b.] /\ the carrier of (Closed-Interval-TSpace a,b) by FUNCT_2:def 1
.= [.a,b.] by A2 ;
rng f c= the carrier of (Closed-Interval-TSpace c,d) ;
then rng f c= [.c,d.] by A1, TOPMETR:25;
then rng f c= REAL by MEMBERED:3;
then reconsider g = f as PartFunc of [.a,b.],REAL by A2, A3, RELSET_1:11;
reconsider g = g as PartFunc of REAL ,REAL by A2, A3, RELSET_1:13;
A5: g | [.a,b.] is continuous by A1, Th15;

per cases ( g | [.a,b.] is increasing or g | [.a,b.] is decreasing ) by A1, A5, A4, XBOOLE_1:18, FCONT_2:18;

suppose A6: g | [.a,b.] is increasing ; :: thesis: for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy

for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy

proof

let x, y be Point of (Closed-Interval-TSpace a,b); :: thesis: for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy
let p, q, fx, fy be Real; :: thesis: ( x = p & y = q & p < q & fx = f . x & fy = f . y implies fx < fy )
A7: ( x in the carrier of (Closed-Interval-TSpace a,b) & y in the carrier of (Closed-Interval-TSpace a,b) ) ;
assume A8: ( x = p & y = q & p < q & fx = f . x & fy = f . y ) ; :: thesis: fx < fy
then ( p in [.a,b.] /\ (dom g) & q in [.a,b.] /\ (dom g) ) by A1, A4, A7, TOPMETR:25;
hence fx < fy by A6, A8, RFUNCT_2:43; :: thesis: verum

end;

hence for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy ; :: thesis: verum

end;

suppose A9: g | [.a,b.] is decreasing ; :: thesis: for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy

( a in [.a,b.] /\ (dom g) & b in [.a,b.] /\ (dom g) & a < b ) by A1, A2, A4, Lm6;
hence for x, y being Point of (Closed-Interval-TSpace a,b)
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy by A1, A9, RFUNCT_2:44; :: thesis: verum

end;

end;