let a, b, c, d be Real; for ar, br, cr, dr being Point of (Trectangle (a,b,c,d))
for h being Path of ar,br
for v being Path of dr,cr
for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds
ex s, t being Point of I[01] st h . s = v . t
let ar, br, cr, dr be Point of (Trectangle (a,b,c,d)); for h being Path of ar,br
for v being Path of dr,cr
for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds
ex s, t being Point of I[01] st h . s = v . t
let h be Path of ar,br; for v being Path of dr,cr
for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds
ex s, t being Point of I[01] st h . s = v . t
let v be Path of dr,cr; for Ar, Br, Cr, Dr being Point of (TOP-REAL 2) st Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr holds
ex s, t being Point of I[01] st h . s = v . t
let Ar, Br, Cr, Dr be Point of (TOP-REAL 2); ( Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr implies ex s, t being Point of I[01] st h . s = v . t )
assume A1:
( Ar `1 = a & Br `1 = b & Cr `2 = c & Dr `2 = d & ar = Ar & br = Br & cr = Cr & dr = Dr )
; ex s, t being Point of I[01] st h . s = v . t
set TR = Trectangle (a,b,c,d);
per cases
( Trectangle (a,b,c,d) is empty or not Trectangle (a,b,c,d) is empty )
;
suppose
not
Trectangle (
a,
b,
c,
d) is
empty
;
ex s, t being Point of I[01] st h . s = v . tthen reconsider TR =
Trectangle (
a,
b,
c,
d) as non
empty convex SubSpace of
TOP-REAL 2 ;
reconsider ar =
ar,
br =
br,
cr =
cr,
dr =
dr as
Point of
TR ;
reconsider h =
h as
Path of
ar,
br ;
reconsider v =
v as
Path of
dr,
cr ;
A3:
(
h . 0 = ar &
h . 1
= br )
by BORSUK_2:def 4;
the
carrier of
TR is
Subset of
(TOP-REAL 2)
by TSEP_1:1;
then reconsider f =
h,
g =
- v as
Function of
I[01],
(TOP-REAL 2) by FUNCT_2:7;
A4:
(
(- v) . 0 = cr &
(- v) . 1
= dr )
by BORSUK_2:def 4;
A5:
for
r being
Point of
I[01] holds
(
a <= (f . r) `1 &
(f . r) `1 <= b &
a <= (g . r) `1 &
(g . r) `1 <= b &
c <= (f . r) `2 &
(f . r) `2 <= d &
c <= (g . r) `2 &
(g . r) `2 <= d )
(
f is
continuous &
g is
continuous )
by PRE_TOPC:26;
then
rng f meets rng g
by A1, A3, A4, A5, Th5, BORSUK_1:def 14, BORSUK_1:def 15;
then consider y being
object such that A8:
y in rng f
and A9:
y in rng g
by XBOOLE_0:3;
consider t being
object such that A10:
t in dom g
and A11:
g . t = y
by A9, FUNCT_1:def 3;
consider s being
object such that A12:
s in dom f
and A13:
f . s = y
by A8, FUNCT_1:def 3;
reconsider s =
s,
t =
t as
Point of
I[01] by A12, A10;
reconsider t1 = 1
- t as
Point of
I[01] by JORDAN5B:4;
take
s
;
ex t being Point of I[01] st h . s = v . ttake
t1
;
h . s = v . t1
dr,
cr are_connected
by BORSUK_2:def 3;
hence
h . s = v . t1
by A13, A11, BORSUK_2:def 6;
verum end; end;