theorem Th126:
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
Real for
f,
g being
Function of
I[01],
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle (
a,
b,
c,
d) &
rng g c= closed_inside_of_rectangle (
a,
b,
c,
d) holds
rng f meets rng g