let a, b, c, d be Real; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 A2: Trectangle (a,b,c,d) is empty ; :: thesis: ex s, t being Point of I[01] st h . s = v . t
take 1[01] ; :: thesis: ex t being Point of I[01] st h . 1[01] = v . t
take 1[01] ; :: thesis: h . 1[01] = v . 1[01]
thus h . 1[01] = v . 1[01] by A2; :: thesis: verum
end;
suppose not Trectangle (a,b,c,d) is empty ; :: thesis: ex s, t being Point of I[01] st h . s = v . t
then 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 )
proof
let r be Point of I[01]; :: thesis: ( 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 )
A6: the carrier of TR = closed_inside_of_rectangle (a,b,c,d) by PRE_TOPC:8
.= { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } by JGRAPH_6:def 2 ;
(- v) . r in the carrier of TR ;
then A7: ex p being Point of (TOP-REAL 2) st
( (- v) . r = p & a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A6;
h . r in the carrier of TR ;
then ex p being Point of (TOP-REAL 2) st
( h . r = p & a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A6;
hence ( 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 ) by A7; :: thesis: verum
end;
( 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 ; :: thesis: ex t being Point of I[01] st h . s = v . t
take t1 ; :: thesis: 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; :: thesis: verum
end;
end;