let a, b, c, d be Real; :: thesis: for f, g being continuous Function of I[01],(TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( 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 ) ) holds
rng f meets rng g
let f, g be continuous Function of I[01],(TOP-REAL 2); :: thesis: for O, I being Point of I[01] st O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( 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 ) ) holds
rng f meets rng g
let O, I be Point of I[01]; :: thesis: ( O = 0 & I = 1 & (f . O) `1 = a & (f . I) `1 = b & (g . O) `2 = c & (g . I) `2 = d & ( 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 ) ) implies rng f meets rng g )
assume that
A1: ( O = 0 & I = 1 ) and
A2: (f . O) `1 = a and
A3: (f . I) `1 = b and
A4: (g . O) `2 = c and
A5: (g . I) `2 = d and
A6: 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 ) ; :: thesis: rng f meets rng g
reconsider Q = rng g as non empty Subset of (TOP-REAL 2) ;
A7: the carrier of ((TOP-REAL 2) | Q) = [#] ((TOP-REAL 2) | Q)
.= rng g by PRE_TOPC:def 5 ;
dom g = the carrier of I[01] by FUNCT_2:def 1;
then reconsider g1 = g as Function of I[01],((TOP-REAL 2) | Q) by A7, FUNCT_2:1;
reconsider q2 = g1 . I as Point of (TOP-REAL 2) by A5;
reconsider q1 = g1 . O as Point of (TOP-REAL 2) by A4;
reconsider P = rng f as non empty Subset of (TOP-REAL 2) ;
A8: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= rng f by PRE_TOPC:def 5 ;
dom f = the carrier of I[01] by FUNCT_2:def 1;
then reconsider f1 = f as Function of I[01],((TOP-REAL 2) | P) by A8, FUNCT_2:1;
reconsider p2 = f1 . I as Point of (TOP-REAL 2) by A3;
reconsider p1 = f1 . O as Point of (TOP-REAL 2) by A2;
A9: for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in P implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) )
assume p in P ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )
then ex x being object st
( x in dom f1 & p = f1 . x ) by FUNCT_1:def 3;
hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A2, A3, A6; :: thesis: verum
end;
A10: for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in P implies ( q1 `2 <= p `2 & p `2 <= q2 `2 ) )
assume p in P ; :: thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 )
then ex x being object st
( x in dom f1 & p = f1 . x ) by FUNCT_1:def 3;
hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A4, A5, A6; :: thesis: verum
end;
A11: for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 )
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in Q implies ( q1 `2 <= p `2 & p `2 <= q2 `2 ) )
assume p in Q ; :: thesis: ( q1 `2 <= p `2 & p `2 <= q2 `2 )
then ex x being object st
( x in dom g1 & p = g1 . x ) by FUNCT_1:def 3;
hence ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A4, A5, A6; :: thesis: verum
end;
A12: for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
proof
let p be Point of (TOP-REAL 2); :: thesis: ( p in Q implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) )
assume p in Q ; :: thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )
then ex x being object st
( x in dom g1 & p = g1 . x ) by FUNCT_1:def 3;
hence ( p1 `1 <= p `1 & p `1 <= p2 `1 ) by A2, A3, A6; :: thesis: verum
end;
( f is Path of p1,p2 & g is Path of q1,q2 ) by A1, BORSUK_2:def 4;
hence rng f meets rng g by A9, A12, A10, A11, Th4; :: thesis: verum