let f be one-to-one continuous Function of R^1,R^1; :: thesis: ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )
A1: [.0,1.] /\ (dom f) = [.0,1.] /\ the carrier of R^1 by FUNCT_2:def 1
.= [.0,1.] by BORSUK_1:35, BORSUK_1:83, TOPMETR:27, XBOOLE_1:28 ;
reconsider g = f as PartFunc of REAL,REAL by TOPMETR:24;

per cases ( g | [.0,1.] is increasing or g | [.0,1.] is decreasing ) by Lm5;

suppose g | [.0,1.] is increasing ; :: thesis: ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )

hence ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
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, BORSUK_1:83, RFUNCT_2:43; :: thesis: verum

end;

suppose g | [.0,1.] is decreasing ; :: thesis: ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx > fy )

hence ( for x, y being Point of I[01]
for p, q, fx, fy being Real st x = p & y = q & p < q & fx = f . x & fy = f . y holds
fx < fy or for x, y being Point of I[01]
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, BORSUK_1:83, RFUNCT_2:44; :: thesis: verum

end;

end;