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:1, BORSUK_1:40, TOPMETR:20, XBOOLE_1:28 ;
reconsider g = f as PartFunc of REAL,REAL by TOPMETR:17;
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:40, RFUNCT_2:20; :: 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:40, RFUNCT_2:21; :: thesis: verum
end;
end;