theorem
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) st
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (
(- 1),1,
(- 1),1) holds
for
f,
g being
Function of
I[01],
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
rng f c= closed_inside_of_rectangle (
(- 1),1,
(- 1),1) &
rng g c= closed_inside_of_rectangle (
(- 1),1,
(- 1),1) holds
rng f meets rng g