:: JGRAPH_8 semantic presentation
begin
Lm1: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:20, TOPMETR:def_7;
Lm2: for x being set
for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
proof
let x be set ; ::_thesis: for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
let f be FinSequence; ::_thesis: ( 1 <= len f implies ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) )
assume A1: 1 <= len f ; ::_thesis: ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
then A2: len f in dom f by FINSEQ_3:25;
A3: (<*x*> ^ f) . ((len f) + 1) = (<*x*> ^ f) . ((len <*x*>) + (len f)) by FINSEQ_1:39
.= f . (len f) by A2, FINSEQ_1:def_7 ;
1 in dom f by A1, FINSEQ_3:25;
hence ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) by A3, FINSEQ_1:def_7; ::_thesis: verum
end;
Lm3: for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) holds
f is increasing
proof
let f be FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) implies f is increasing )
assume A1: for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ; ::_thesis: f is increasing
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_i_<_j_holds_
f_._i_<_f_._j
let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )
now__::_thesis:_(_i_in_dom_f_&_j_in_dom_f_&_i_<_j_implies_f_._i_<_f_._j_)
defpred S1[ Element of NAT ] means ( i + (1 + $1) <= len f implies f /. i < f /. (i + (1 + $1)) );
assume that
A2: i in dom f and
A3: j in dom f and
A4: i < j ; ::_thesis: f . i < f . j
A5: 1 <= i by A2, FINSEQ_3:25;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; ::_thesis: S1[k + 1]
now__::_thesis:_(_i_+_(1_+_(k_+_1))_<=_len_f_implies_f_/._i_<_f_/._(i_+_(1_+_(k_+_1)))_)
( 1 <= i + 1 & i + 1 <= (i + 1) + k ) by NAT_1:11;
then A8: 1 <= (i + 1) + k by XXREAL_0:2;
A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ;
1 + k < 1 + (k + 1) by NAT_1:13;
then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6;
assume A11: i + (1 + (k + 1)) <= len f ; ::_thesis: f /. i < f /. (i + (1 + (k + 1)))
then i + (1 + k) < len f by A10, XXREAL_0:2;
then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A8, A9;
hence f /. i < f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
i + 1 <= j by A4, NAT_1:13;
then j -' (i + 1) = j - (i + 1) by XREAL_1:233;
then A12: i + (1 + (j -' (i + 1))) = j ;
A13: f /. i = f . i by A2, PARTFUN1:def_6;
A14: j <= len f by A3, FINSEQ_3:25;
then i < len f by A4, XXREAL_0:2;
then A15: S1[ 0 ] by A1, A5;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A6);
then f /. i < f /. j by A14, A12;
hence f . i < f . j by A3, A13, PARTFUN1:def_6; ::_thesis: verum
end;
hence ( i in dom f & j in dom f & i < j implies f . i < f . j ) ; ::_thesis: verum
end;
hence f is increasing by SEQM_3:def_1; ::_thesis: verum
end;
registration
let a, b, c, d be real number ;
cluster closed_inside_of_rectangle (a,b,c,d) -> convex ;
coherence
closed_inside_of_rectangle (a,b,c,d) is convex
proof
set P = closed_inside_of_rectangle (a,b,c,d);
A1: closed_inside_of_rectangle (a,b,c,d) = { 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;
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def_1 ::_thesis: ( not w1 in closed_inside_of_rectangle (a,b,c,d) or not w2 in closed_inside_of_rectangle (a,b,c,d) or LSeg (w1,w2) c= closed_inside_of_rectangle (a,b,c,d) )
assume ( w1 in closed_inside_of_rectangle (a,b,c,d) & w2 in closed_inside_of_rectangle (a,b,c,d) ) ; ::_thesis: LSeg (w1,w2) c= closed_inside_of_rectangle (a,b,c,d)
then A2: ( ex p3 being Point of (TOP-REAL 2) st
( p3 = w1 & a <= p3 `1 & p3 `1 <= b & c <= p3 `2 & p3 `2 <= d ) & ex p4 being Point of (TOP-REAL 2) st
( p4 = w2 & a <= p4 `1 & p4 `1 <= b & c <= p4 `2 & p4 `2 <= d ) ) by A1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (w1,w2) or x in closed_inside_of_rectangle (a,b,c,d) )
assume x in LSeg (w1,w2) ; ::_thesis: x in closed_inside_of_rectangle (a,b,c,d)
then consider l being Real such that
A3: x = ((1 - l) * w1) + (l * w2) and
A4: ( 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A5: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55;
A6: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A7: (l * w2) `2 = l * (w2 `2) by EUCLID:52;
A8: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57;
then ((1 - l) * w1) `2 = (1 - l) * (w1 `2) by EUCLID:52;
then (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A5, A7, EUCLID:52;
then A9: ( c <= (((1 - l) * w1) + (l * w2)) `2 & (((1 - l) * w1) + (l * w2)) `2 <= d ) by A2, A4, XREAL_1:173, XREAL_1:174;
A10: (l * w2) `1 = l * (w2 `1) by A6, EUCLID:52;
((1 - l) * w1) `1 = (1 - l) * (w1 `1) by A8, EUCLID:52;
then (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A5, A10, EUCLID:52;
then ( a <= (((1 - l) * w1) + (l * w2)) `1 & (((1 - l) * w1) + (l * w2)) `1 <= b ) by A2, A4, XREAL_1:173, XREAL_1:174;
hence x in closed_inside_of_rectangle (a,b,c,d) by A1, A3, A9; ::_thesis: verum
end;
end;
registration
let a, b, c, d be real number ;
cluster Trectangle (a,b,c,d) -> convex ;
coherence
Trectangle (a,b,c,d) is convex
proof
set T = Trectangle (a,b,c,d);
thus [#] (Trectangle (a,b,c,d)) is convex Subset of (TOP-REAL 2) by PRE_TOPC:8; :: according to TOPALG_2:def_1 ::_thesis: verum
end;
end;
theorem Th1: :: JGRAPH_8:1
for n being Element of NAT
for e being real positive number
for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
proof
let n be Element of NAT ; ::_thesis: for e being real positive number
for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A1: 1 in [.0,1.] by RCOMP_1:def_1;
{1} c= [.0,1.]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in [.0,1.] )
assume x in {1} ; ::_thesis: x in [.0,1.]
hence x in [.0,1.] by A1, TARSKI:def_1; ::_thesis: verum
end;
then A2: [.0,1.] \/ {1} = [.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7;
then A3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20
.= [.0,1.] by TOPMETR:10 ;
let e be real positive number ; ::_thesis: for g being continuous Function of I[01],(TOP-REAL n) ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
let g be continuous Function of I[01],(TOP-REAL n); ::_thesis: ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )
reconsider e = e as positive Real by XREAL_0:def_1;
reconsider f = g as Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by UNIFORM1:10;
A4: e / 2 < e by XREAL_1:216;
A5: e / 2 > 0 by XREAL_1:215;
f is uniformly_continuous by UNIFORM1:8;
then consider s1 being Real such that
A6: 0 < s1 and
A7: for u1, u2 being Element of (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < s1 holds
dist ((f /. u1),(f /. u2)) < e / 2 by A5, UNIFORM1:def_1;
set s = min (s1,(1 / 2));
defpred S1[ Nat, set ] means $2 = ((min (s1,(1 / 2))) / 2) * ($1 - 1);
A8: 0 <= min (s1,(1 / 2)) by A6, XXREAL_0:20;
then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Element of NAT by INT_1:53;
A9: 2 / (min (s1,(1 / 2))) <= j by INT_1:def_7;
A10: min (s1,(1 / 2)) <= s1 by XXREAL_0:17;
A11: for u1, u2 being Element of (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < min (s1,(1 / 2)) holds
dist ((f /. u1),(f /. u2)) < e / 2
proof
let u1, u2 be Element of (Closed-Interval-MSpace (0,1)); ::_thesis: ( dist (u1,u2) < min (s1,(1 / 2)) implies dist ((f /. u1),(f /. u2)) < e / 2 )
assume dist (u1,u2) < min (s1,(1 / 2)) ; ::_thesis: dist ((f /. u1),(f /. u2)) < e / 2
then dist (u1,u2) < s1 by A10, XXREAL_0:2;
hence dist ((f /. u1),(f /. u2)) < e / 2 by A7; ::_thesis: verum
end;
A12: 2 / (min (s1,(1 / 2))) <= [/(2 / (min (s1,(1 / 2))))\] by INT_1:def_7;
then (2 / (min (s1,(1 / 2)))) - j <= 0 by XREAL_1:47;
then 1 + ((2 / (min (s1,(1 / 2)))) - j) <= 1 + 0 by XREAL_1:6;
then A13: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by A8, XREAL_1:64;
A14: for k being Nat st k in Seg j holds
ex x being set st S1[k,x] ;
consider p being FinSequence such that
A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A14);
A16: Seg (len p) = Seg j by A15, FINSEQ_1:def_3;
rng (p ^ <*1*>) c= REAL
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^ <*1*>) or y in REAL )
A17: len (p ^ <*1*>) = (len p) + 1 by FINSEQ_2:16;
assume y in rng (p ^ <*1*>) ; ::_thesis: y in REAL
then consider x being set such that
A18: x in dom (p ^ <*1*>) and
A19: y = (p ^ <*1*>) . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A18;
A20: dom (p ^ <*1*>) = Seg (len (p ^ <*1*>)) by FINSEQ_1:def_3;
then A21: 1 <= nx by A18, FINSEQ_1:1;
A22: 1 <= nx by A18, A20, FINSEQ_1:1;
A23: nx <= len (p ^ <*1*>) by A18, A20, FINSEQ_1:1;
percases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ;
suppose nx < (len p) + 1 ; ::_thesis: y in REAL
then A24: nx <= len p by NAT_1:13;
then nx in Seg j by A16, A22, FINSEQ_1:1;
then A25: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A15;
y = p . nx by A19, A21, A24, FINSEQ_1:64;
hence y in REAL by A25; ::_thesis: verum
end;
suppose nx >= (len p) + 1 ; ::_thesis: y in REAL
then nx = (len p) + 1 by A23, A17, XXREAL_0:1;
then y = 1 by A19, FINSEQ_1:42;
hence y in REAL ; ::_thesis: verum
end;
end;
end;
then reconsider h1 = p ^ <*1*> as FinSequence of REAL by FINSEQ_1:def_4;
A26: len h1 = (len p) + 1 by FINSEQ_2:16;
A27: len p = j by A15, FINSEQ_1:def_3;
A28: min (s1,(1 / 2)) <> 0 by A6, XXREAL_0:15;
then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by A8, XREAL_1:118, XXREAL_0:17;
then 4 <= j by A9, XXREAL_0:2;
then A29: 4 + 1 <= (len p) + 1 by A27, XREAL_1:6;
A30: (min (s1,(1 / 2))) / 2 > 0 by A8, A28, XREAL_1:215;
A31: for i being Element of NAT
for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
proof
let i be Element of NAT ; ::_thesis: for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
let r1, r2 be Real; ::_thesis: ( 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) implies ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) )
assume that
A32: ( 1 <= i & i < len p ) and
A33: r1 = p . i and
A34: r2 = p . (i + 1) ; ::_thesis: ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 )
( 1 < i + 1 & i + 1 <= len p ) by A32, NAT_1:13;
then i + 1 in Seg j by A16, FINSEQ_1:1;
then A35: r2 = ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A15, A34;
i < i + 1 by NAT_1:13;
then A36: i - 1 < (i + 1) - 1 by XREAL_1:9;
A37: i in Seg j by A16, A32, FINSEQ_1:1;
then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A15, A33;
hence r1 < r2 by A30, A35, A36, XREAL_1:68; ::_thesis: r2 - r1 = (min (s1,(1 / 2))) / 2
r2 - r1 = (((min (s1,(1 / 2))) / 2) * i) - (((min (s1,(1 / 2))) / 2) * (i - 1)) by A15, A33, A37, A35;
hence r2 - r1 = (min (s1,(1 / 2))) / 2 ; ::_thesis: verum
end;
0 < min (s1,(1 / 2)) by A6, A28, XXREAL_0:20;
then 0 < j by A12, XREAL_1:139;
then A38: 0 + 1 <= j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p . 1 = ((min (s1,(1 / 2))) / 2) * (1 - 1) by A15
.= 0 ;
then A39: h1 . 1 = 0 by A38, A27, Lm2;
2 * (min (s1,(1 / 2))) <> 0 by A6, XXREAL_0:15;
then A40: ( ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) = (2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) & (2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) = 1 ) by XCMPLX_1:60, XCMPLX_1:76;
then A41: 1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) = ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) ;
A42: for r1 being Real st r1 = p . (len p) holds
1 - r1 <= (min (s1,(1 / 2))) / 2
proof
let r1 be Real; ::_thesis: ( r1 = p . (len p) implies 1 - r1 <= (min (s1,(1 / 2))) / 2 )
assume A43: r1 = p . (len p) ; ::_thesis: 1 - r1 <= (min (s1,(1 / 2))) / 2
len p in Seg j by A38, A27, FINSEQ_1:1;
hence 1 - r1 <= (min (s1,(1 / 2))) / 2 by A13, A15, A27, A41, A43; ::_thesis: verum
end;
A44: for i being Element of NAT st 1 <= i & i < len h1 holds
(h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 )
assume that
A45: 1 <= i and
A46: i < len h1 ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
A47: i + 1 <= len h1 by A46, NAT_1:13;
A48: i <= len p by A26, A46, NAT_1:13;
A49: 1 < i + 1 by A45, NAT_1:13;
percases ( i < len p or i >= len p ) ;
supposeA50: i < len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
then i + 1 <= len p by NAT_1:13;
then A51: h1 . (i + 1) = p . (i + 1) by A49, FINSEQ_1:64;
A52: h1 . i = p . i by A45, A50, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A45, A46, A47, A49, FINSEQ_4:15;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A31, A45, A50, A52, A51; ::_thesis: verum
end;
suppose i >= len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2
then A53: i = len p by A48, XXREAL_0:1;
A54: h1 /. i = h1 . i by A45, A46, FINSEQ_4:15
.= p . i by A45, A48, FINSEQ_1:64 ;
h1 /. (i + 1) = h1 . (i + 1) by A47, A49, FINSEQ_4:15
.= 1 by A53, FINSEQ_1:42 ;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A42, A53, A54; ::_thesis: verum
end;
end;
end;
[/(2 / (min (s1,(1 / 2))))\] < (2 / (min (s1,(1 / 2)))) + 1 by INT_1:def_7;
then [/(2 / (min (s1,(1 / 2))))\] - 1 < ((2 / (min (s1,(1 / 2)))) + 1) - 1 by XREAL_1:9;
then A55: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A30, XREAL_1:68;
A56: for i being Element of NAT
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
r1 < 1
proof
let i be Element of NAT ; ::_thesis: for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
r1 < 1
let r1 be Real; ::_thesis: ( 1 <= i & i <= len p & r1 = p . i implies r1 < 1 )
assume that
A57: 1 <= i and
A58: i <= len p and
A59: r1 = p . i ; ::_thesis: r1 < 1
i - 1 <= j - 1 by A27, A58, XREAL_1:9;
then A60: ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A8, XREAL_1:64;
i in Seg j by A16, A57, A58, FINSEQ_1:1;
then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A15, A59;
hence r1 < 1 by A55, A40, A60, XXREAL_0:2; ::_thesis: verum
end;
A61: for i being Element of NAT st 1 <= i & i < len h1 holds
h1 /. i < h1 /. (i + 1)
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len h1 implies h1 /. i < h1 /. (i + 1) )
assume that
A62: 1 <= i and
A63: i < len h1 ; ::_thesis: h1 /. i < h1 /. (i + 1)
A64: i + 1 <= len h1 by A63, NAT_1:13;
A65: 1 < i + 1 by A62, NAT_1:13;
A66: i <= len p by A26, A63, NAT_1:13;
percases ( i < len p or i >= len p ) ;
supposeA67: i < len p ; ::_thesis: h1 /. i < h1 /. (i + 1)
then i + 1 <= len p by NAT_1:13;
then A68: h1 . (i + 1) = p . (i + 1) by A65, FINSEQ_1:64;
A69: h1 . i = p . i by A62, A67, FINSEQ_1:64;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A62, A63, A64, A65, FINSEQ_4:15;
hence h1 /. i < h1 /. (i + 1) by A31, A62, A67, A69, A68; ::_thesis: verum
end;
suppose i >= len p ; ::_thesis: h1 /. i < h1 /. (i + 1)
then A70: i = len p by A66, XXREAL_0:1;
A71: h1 /. (i + 1) = h1 . (i + 1) by A64, A65, FINSEQ_4:15
.= 1 by A70, FINSEQ_1:42 ;
h1 /. i = h1 . i by A62, A63, FINSEQ_4:15
.= p . i by A62, A66, FINSEQ_1:64 ;
hence h1 /. i < h1 /. (i + 1) by A56, A62, A66, A71; ::_thesis: verum
end;
end;
end;
A72: dom g = the carrier of I[01] by FUNCT_2:def_1;
A73: for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e
proof
let i be Element of NAT ; ::_thesis: for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e
let Q be Subset of I[01]; ::_thesis: for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e
let W be Subset of (Euclid n); ::_thesis: ( 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q implies diameter W < e )
assume that
A74: ( 1 <= i & i < len h1 ) and
A75: Q = [.(h1 /. i),(h1 /. (i + 1)).] and
A76: W = g .: Q ; ::_thesis: diameter W < e
h1 /. i < h1 /. (i + 1) by A61, A74;
then A77: Q <> {} by A75, XXREAL_1:1;
A78: for x, y being Point of (Euclid n) st x in W & y in W holds
dist (x,y) <= e / 2
proof
let x, y be Point of (Euclid n); ::_thesis: ( x in W & y in W implies dist (x,y) <= e / 2 )
assume that
A79: x in W and
A80: y in W ; ::_thesis: dist (x,y) <= e / 2
consider x3 being set such that
A81: x3 in dom g and
A82: x3 in Q and
A83: x = g . x3 by A76, A79, FUNCT_1:def_6;
reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A81, Lm1, TOPMETR:12;
reconsider r3 = x3 as Real by A75, A82;
A84: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A44, A74;
consider y3 being set such that
A85: y3 in dom g and
A86: y3 in Q and
A87: y = g . y3 by A76, A80, FUNCT_1:def_6;
reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A85, Lm1, TOPMETR:12;
reconsider s3 = y3 as Real by A75, A86;
A88: ( f . x3 = f /. x3 & f . y3 = f /. y3 ) ;
abs (r3 - s3) <= (h1 /. (i + 1)) - (h1 /. i) by A75, A82, A86, UNIFORM1:12;
then abs (r3 - s3) <= (min (s1,(1 / 2))) / 2 by A84, XXREAL_0:2;
then A89: dist (x3,y3) <= (min (s1,(1 / 2))) / 2 by HEINE:1;
(min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) by A8, A28, XREAL_1:216;
then dist (x3,y3) < min (s1,(1 / 2)) by A89, XXREAL_0:2;
hence dist (x,y) <= e / 2 by A11, A83, A87, A88; ::_thesis: verum
end;
then W is bounded by A5, TBSP_1:def_7;
then diameter W <= e / 2 by A72, A76, A77, A78, TBSP_1:def_8;
hence diameter W < e by A4, XXREAL_0:2; ::_thesis: verum
end;
A90: rng p c= [.0,1.]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in [.0,1.] )
assume y in rng p ; ::_thesis: y in [.0,1.]
then consider x being set such that
A91: x in dom p and
A92: y = p . x by FUNCT_1:def_3;
reconsider nx = x as Element of NAT by A91;
A93: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A15, A91;
then reconsider ry = p . nx as Real ;
A94: x in Seg (len p) by A91, FINSEQ_1:def_3;
then A95: 1 <= nx by FINSEQ_1:1;
then A96: nx - 1 >= 1 - 1 by XREAL_1:9;
nx <= len p by A94, FINSEQ_1:1;
then ry < 1 by A56, A95;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A8, A92, A93, A96;
hence y in [.0,1.] by RCOMP_1:def_1; ::_thesis: verum
end;
rng <*1*> = {1} by FINSEQ_1:38;
then rng h1 = (rng p) \/ {1} by FINSEQ_1:31;
then A97: rng h1 c= [.0,1.] \/ {1} by A90, XBOOLE_1:13;
h1 . (len h1) = 1 by A26, FINSEQ_1:42;
hence ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) ) by A26, A29, A39, A2, A97, A3, A61, A73, Lm3; ::_thesis: verum
end;
theorem Th2: :: JGRAPH_8:2
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds
P = LSeg (p1,p2)
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds
P = LSeg (p1,p2)
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected holds
P = LSeg (p1,p2)
let P be Subset of (TOP-REAL n); ::_thesis: ( P c= LSeg (p1,p2) & p1 in P & p2 in P & P is connected implies P = LSeg (p1,p2) )
assume that
A1: P c= LSeg (p1,p2) and
A2: p1 in P and
A3: p2 in P and
A4: P is connected ; ::_thesis: P = LSeg (p1,p2)
reconsider L = LSeg (p1,p2) as non empty Subset of (TOP-REAL n) by A1, A2;
now__::_thesis:_LSeg_(p1,p2)_c=_P
A5: the carrier of ((TOP-REAL n) | L) = [#] ((TOP-REAL n) | L)
.= L by PRE_TOPC:def_5 ;
then reconsider PX = P as Subset of ((TOP-REAL n) | L) by A1;
assume not LSeg (p1,p2) c= P ; ::_thesis: contradiction
then consider x0 being set such that
A6: x0 in LSeg (p1,p2) and
A7: not x0 in P by TARSKI:def_3;
reconsider p0 = x0 as Point of (TOP-REAL n) by A6;
A8: (LSeg (p0,p2)) \ {p0} c= LSeg (p0,p2) by XBOOLE_1:36;
A9: p1 in LSeg (p1,p2) by RLTOPSP1:68;
then reconsider PX1 = LSeg (p1,p0) as Subset of ((TOP-REAL n) | L) by A6, A5, TOPREAL1:6;
A10: (LSeg (p1,p0)) \ {p0} c= LSeg (p1,p0) by XBOOLE_1:36;
LSeg (p1,p0) c= L by A6, A9, TOPREAL1:6;
then reconsider R1 = (LSeg (p1,p0)) \ {p0} as Subset of ((TOP-REAL n) | L) by A10, A5, XBOOLE_1:1;
A11: (TOP-REAL n) | L is T_2 by TOPMETR:2;
A12: p2 in LSeg (p1,p2) by RLTOPSP1:68;
then LSeg (p0,p2) c= L by A6, TOPREAL1:6;
then reconsider R2 = (LSeg (p0,p2)) \ {p0} as Subset of ((TOP-REAL n) | L) by A5, A8, XBOOLE_1:1;
reconsider PX2 = LSeg (p0,p2) as Subset of ((TOP-REAL n) | L) by A6, A5, A12, TOPREAL1:6;
A13: PX1 /\ PX2 = {p0} by A6, TOPREAL1:8;
A14: R1 c= PX1 by XBOOLE_1:36;
A15: now__::_thesis:_not_P_c=_R1
assume P c= R1 ; ::_thesis: contradiction
then A16: p2 in R1 by A3;
p2 in PX2 by RLTOPSP1:68;
then p2 in PX1 /\ PX2 by A14, A16, XBOOLE_0:def_4;
hence contradiction by A3, A7, A13, TARSKI:def_1; ::_thesis: verum
end;
A17: {p0} c= LSeg (p1,p0)
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in {p0} or d in LSeg (p1,p0) )
assume d in {p0} ; ::_thesis: d in LSeg (p1,p0)
then d = p0 by TARSKI:def_1;
hence d in LSeg (p1,p0) by RLTOPSP1:68; ::_thesis: verum
end;
A18: {p0} c= LSeg (p0,p2)
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in {p0} or d in LSeg (p0,p2) )
assume d in {p0} ; ::_thesis: d in LSeg (p0,p2)
then d = p0 by TARSKI:def_1;
hence d in LSeg (p0,p2) by RLTOPSP1:68; ::_thesis: verum
end;
PX2 is compact by COMPTS_1:19;
then PX2 is closed by A11, COMPTS_1:7;
then A19: Cl PX2 = PX2 by PRE_TOPC:22;
A20: Cl R2 c= Cl PX2 by PRE_TOPC:19, XBOOLE_1:36;
R1 /\ PX2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49
.= {} by A13, XBOOLE_1:37 ;
then R1 /\ (Cl R2) = {} by A19, A20, XBOOLE_1:3, XBOOLE_1:27;
then A21: R1 misses Cl R2 by XBOOLE_0:def_7;
A22: PX1 /\ PX2 = {p0} by A6, TOPREAL1:8;
A23: R2 c= PX2 by XBOOLE_1:36;
A24: now__::_thesis:_not_P_c=_R2
assume P c= R2 ; ::_thesis: contradiction
then A25: p1 in R2 by A2;
p1 in PX1 by RLTOPSP1:68;
then p1 in PX1 /\ PX2 by A23, A25, XBOOLE_0:def_4;
hence contradiction by A2, A7, A13, TARSKI:def_1; ::_thesis: verum
end;
PX1 is compact by COMPTS_1:19;
then PX1 is closed by A11, COMPTS_1:7;
then A26: Cl PX1 = PX1 by PRE_TOPC:22;
A27: L = (LSeg (p1,p0)) \/ (LSeg (p0,p2)) by A6, TOPREAL1:5
.= (((LSeg (p1,p0)) \ {p0}) \/ {p0}) \/ (LSeg (p0,p2)) by A17, XBOOLE_1:45
.= ((LSeg (p1,p0)) \ {p0}) \/ ({p0} \/ (LSeg (p0,p2))) by XBOOLE_1:4
.= R1 \/ PX2 by A18, XBOOLE_1:12
.= R1 \/ ((PX2 \ {p0}) \/ {p0}) by A18, XBOOLE_1:45
.= (R1 \/ {p0}) \/ R2 by XBOOLE_1:4 ;
A28: P c= R1 \/ R2
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in P or z in R1 \/ R2 )
assume A29: z in P ; ::_thesis: z in R1 \/ R2
then ( z in R1 \/ {p0} or z in R2 ) by A1, A27, XBOOLE_0:def_3;
then ( z in R1 or z in {p0} or z in R2 ) by XBOOLE_0:def_3;
hence z in R1 \/ R2 by A7, A29, TARSKI:def_1, XBOOLE_0:def_3; ::_thesis: verum
end;
A30: Cl R1 c= Cl PX1 by PRE_TOPC:19, XBOOLE_1:36;
PX1 /\ R2 = (PX1 /\ PX2) \ {p0} by XBOOLE_1:49
.= {} by A22, XBOOLE_1:37 ;
then (Cl R1) /\ R2 = {} by A26, A30, XBOOLE_1:3, XBOOLE_1:27;
then Cl R1 misses R2 by XBOOLE_0:def_7;
then A31: R1,R2 are_separated by A21, CONNSP_1:def_1;
PX is connected by A4, CONNSP_1:46;
hence contradiction by A31, A28, A15, A24, CONNSP_1:16; ::_thesis: verum
end;
hence P = LSeg (p1,p2) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th3: :: JGRAPH_8:3
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds
rng g = LSeg (p1,p2)
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds
rng g = LSeg (p1,p2)
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for g being Path of p1,p2 st rng g c= LSeg (p1,p2) holds
rng g = LSeg (p1,p2)
let g be Path of p1,p2; ::_thesis: ( rng g c= LSeg (p1,p2) implies rng g = LSeg (p1,p2) )
assume A1: rng g c= LSeg (p1,p2) ; ::_thesis: rng g = LSeg (p1,p2)
A2: p2 = g . 1 by BORSUK_2:def_4;
A3: p1 = g . 0 by BORSUK_2:def_4;
now__::_thesis:_LSeg_(p1,p2)_c=_rng_g
A4: g .: ([#] I[01]) c= rng g
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in g .: ([#] I[01]) or y in rng g )
assume y in g .: ([#] I[01]) ; ::_thesis: y in rng g
then ex x being set st
( x in dom g & x in [#] I[01] & y = g . x ) by FUNCT_1:def_6;
hence y in rng g by FUNCT_1:def_3; ::_thesis: verum
end;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def_1;
then A5: p2 in g .: ([#] I[01]) by A2, FUNCT_1:def_6;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def_1;
then A6: p1 in g .: ([#] I[01]) by A3, FUNCT_1:def_6;
[#] I[01] is connected by CONNSP_1:27;
then A7: g .: ([#] I[01]) is connected by TOPS_2:61;
assume not LSeg (p1,p2) c= rng g ; ::_thesis: contradiction
hence contradiction by A1, A7, A6, A5, A4, Th2, XBOOLE_1:1; ::_thesis: verum
end;
hence rng g = LSeg (p1,p2) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th4: :: JGRAPH_8:4
for P, Q being non empty Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for f being Path of p1,p2
for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
proof
A1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8;
A2: [#] I[01] is compact by COMPTS_1:1;
let P, Q be non empty Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for f being Path of p1,p2
for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: for f being Path of p1,p2
for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
let f be Path of p1,p2; ::_thesis: for g being Path of q1,q2 st rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) holds
P meets Q
let g be Path of q1,q2; ::_thesis: ( rng f = P & rng g = Q & ( for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) & ( for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) & ( for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ) implies P meets Q )
assume that
A3: rng f = P and
A4: rng g = Q and
A5: for p being Point of (TOP-REAL 2) st p in P holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) and
A6: for p being Point of (TOP-REAL 2) st p in Q holds
( p1 `1 <= p `1 & p `1 <= p2 `1 ) and
A7: for p being Point of (TOP-REAL 2) st p in P holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) and
A8: for p being Point of (TOP-REAL 2) st p in Q holds
( q1 `2 <= p `2 & p `2 <= q2 `2 ) ; ::_thesis: P meets Q
TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def_8;
then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid 2)) ;
set e = (min_dist_min (P9,Q9)) / 5;
f .: the carrier of I[01] = rng f by RELSET_1:22;
then P is compact by A3, A2, WEIERSTR:8;
then A9: P9 is compact by A1, COMPTS_1:23;
g .: ([#] I[01]) = rng g by RELSET_1:22;
then Q is compact by A4, A2, WEIERSTR:8;
then A10: Q9 is compact by A1, COMPTS_1:23;
assume A11: P /\ Q = {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then P misses Q by XBOOLE_0:def_7;
then A12: min_dist_min (P9,Q9) > 0 by A10, A9, JGRAPH_1:38;
then A13: (min_dist_min (P9,Q9)) / 5 > 0 / 5 by XREAL_1:74;
then consider h being FinSequence of REAL such that
A14: h . 1 = 0 and
A15: h . (len h) = 1 and
A16: 5 <= len h and
A17: rng h c= the carrier of I[01] and
A18: h is increasing and
A19: for i being Element of NAT
for R being Subset of I[01]
for W being Subset of (Euclid 2) st 1 <= i & i < len h & R = [.(h /. i),(h /. (i + 1)).] & W = f .: R holds
diameter W < (min_dist_min (P9,Q9)) / 5 by Th1;
deffunc H1( Nat) -> set = f . (h . $1);
ex h19 being FinSequence st
( len h19 = len h & ( for i being Nat st i in dom h19 holds
h19 . i = H1(i) ) ) from FINSEQ_1:sch_2();
then consider h19 being FinSequence such that
A20: len h19 = len h and
A21: for i being Nat st i in dom h19 holds
h19 . i = f . (h . i) ;
A22: 1 <= len h by A16, XXREAL_0:2;
then A23: len h in dom h19 by A20, FINSEQ_3:25;
rng h19 c= the carrier of (TOP-REAL 2)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h19 or y in the carrier of (TOP-REAL 2) )
A24: dom f = the carrier of I[01] by FUNCT_2:def_1;
assume y in rng h19 ; ::_thesis: y in the carrier of (TOP-REAL 2)
then consider x being set such that
A25: x in dom h19 and
A26: y = h19 . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A25;
dom h19 = Seg (len h19) by FINSEQ_1:def_3;
then i in dom h by A20, A25, FINSEQ_1:def_3;
then A27: h . i in rng h by FUNCT_1:def_3;
h19 . i = f . (h . i) by A21, A25;
then h19 . i in rng f by A17, A27, A24, FUNCT_1:def_3;
hence y in the carrier of (TOP-REAL 2) by A26; ::_thesis: verum
end;
then reconsider h1 = h19 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def_4;
A28: len h1 >= 1 by A16, A20, XXREAL_0:2;
then A29: h1 . 1 = h1 /. 1 by FINSEQ_4:15;
A30: f . 0 = p1 by BORSUK_2:def_4;
A31: for i being Element of NAT st 1 <= i & i + 1 <= len h1 holds
|.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
proof
reconsider Pa = P as Subset of (TOP-REAL 2) ;
A32: dom f = the carrier of I[01] by FUNCT_2:def_1;
reconsider W1 = P as Subset of (Euclid 2) by TOPREAL3:8;
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len h1 implies |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )
assume that
A33: 1 <= i and
A34: i + 1 <= len h1 ; ::_thesis: |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
A35: 1 < i + 1 by A33, NAT_1:13;
then A36: h . (i + 1) = h /. (i + 1) by A20, A34, FINSEQ_4:15;
A37: i + 1 in dom h19 by A34, A35, FINSEQ_3:25;
then A38: h19 . (i + 1) = f . (h . (i + 1)) by A21;
then A39: h1 /. (i + 1) = f . (h . (i + 1)) by A34, A35, FINSEQ_4:15;
set r1 = (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1;
( [#] I[01] is compact & f .: the carrier of I[01] = rng f ) by COMPTS_1:1, RELSET_1:22;
then A40: Pa is compact by A3, WEIERSTR:8;
A41: for x, y being Point of (Euclid 2) st x in W1 & y in W1 holds
dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
proof
let x, y be Point of (Euclid 2); ::_thesis: ( x in W1 & y in W1 implies dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 )
assume that
A42: x in W1 and
A43: y in W1 ; ::_thesis: dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1
reconsider pw1 = x, pw2 = y as Point of (TOP-REAL 2) by A42, A43;
A44: ( S-bound Pa <= pw2 `2 & pw2 `2 <= N-bound Pa ) by A40, A43, PSCOMP_1:24;
( S-bound Pa <= pw1 `2 & pw1 `2 <= N-bound Pa ) by A40, A42, PSCOMP_1:24;
then A45: abs ((pw1 `2) - (pw2 `2)) <= (N-bound Pa) - (S-bound Pa) by A44, JGRAPH_1:27;
A46: ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by XREAL_1:29;
A47: ( W-bound Pa <= pw2 `1 & pw2 `1 <= E-bound Pa ) by A40, A43, PSCOMP_1:24;
( W-bound Pa <= pw1 `1 & pw1 `1 <= E-bound Pa ) by A40, A42, PSCOMP_1:24;
then abs ((pw1 `1) - (pw2 `1)) <= (E-bound Pa) - (W-bound Pa) by A47, JGRAPH_1:27;
then (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= ((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa)) by A45, XREAL_1:7;
then A48: (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A46, XXREAL_0:2;
( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) ) by JGRAPH_1:28, JGRAPH_1:32;
hence dist (x,y) <= (((E-bound Pa) - (W-bound Pa)) + ((N-bound Pa) - (S-bound Pa))) + 1 by A48, XXREAL_0:2; ::_thesis: verum
end;
i + 1 in dom h by A20, A34, A35, FINSEQ_3:25;
then h . (i + 1) in rng h by FUNCT_1:def_3;
then h19 . (i + 1) in rng f by A17, A38, A32, FUNCT_1:def_3;
then A49: f . (h . (i + 1)) is Element of (TOP-REAL 2) by A21, A37;
A50: i < len h1 by A34, NAT_1:13;
then A51: h . i = h /. i by A20, A33, FINSEQ_4:15;
A52: i in dom h by A20, A33, A50, FINSEQ_3:25;
then A53: h . i in rng h by FUNCT_1:def_3;
A54: i + 1 in dom h by A20, A34, A35, FINSEQ_3:25;
then h . (i + 1) in rng h by FUNCT_1:def_3;
then reconsider R = [.(h /. i),(h /. (i + 1)).] as Subset of I[01] by A17, A53, A51, A36, BORSUK_1:40, XXREAL_2:def_12;
A55: i in dom h19 by A33, A50, FINSEQ_3:25;
then A56: h19 . i = f . (h . i) by A21;
then h19 . i in rng f by A17, A53, A32, FUNCT_1:def_3;
then f . (h . i) is Element of (TOP-REAL 2) by A21, A55;
then reconsider w1 = f . (h . i), w2 = f . (h . (i + 1)) as Point of (Euclid 2) by A49, TOPREAL3:8;
i < i + 1 by NAT_1:13;
then A57: h /. i <= h /. (i + 1) by A18, A52, A51, A54, A36, SEQM_3:def_1;
then h . i in R by A51, XXREAL_1:1;
then A58: w1 in f .: R by A32, FUNCT_1:def_6;
0 in the carrier of I[01] by BORSUK_1:43;
then A59: f . 0 in rng f by A32, FUNCT_1:def_3;
then ( S-bound Pa <= p1 `2 & p1 `2 <= N-bound Pa ) by A3, A30, A40, PSCOMP_1:24;
then S-bound Pa <= N-bound Pa by XXREAL_0:2;
then A60: 0 <= (N-bound Pa) - (S-bound Pa) by XREAL_1:48;
( W-bound Pa <= p1 `1 & p1 `1 <= E-bound Pa ) by A3, A30, A40, A59, PSCOMP_1:24;
then W-bound Pa <= E-bound Pa by XXREAL_0:2;
then 0 <= (E-bound Pa) - (W-bound Pa) by XREAL_1:48;
then A61: W1 is bounded by A60, A41, TBSP_1:def_7;
h . (i + 1) in R by A36, A57, XXREAL_1:1;
then A62: w2 in f .: R by A32, FUNCT_1:def_6;
reconsider W = f .: R as Subset of (Euclid 2) by TOPREAL3:8;
dom f = [#] I[01] by FUNCT_2:def_1;
then P = f .: [.0,1.] by A3, BORSUK_1:40, RELAT_1:113;
then W is bounded by A61, BORSUK_1:40, RELAT_1:123, TBSP_1:14;
then A63: dist (w1,w2) <= diameter W by A58, A62, TBSP_1:def_8;
diameter W < (min_dist_min (P9,Q9)) / 5 by A19, A20, A33, A50;
then A64: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A63, XXREAL_0:2;
h1 /. i = f . (h . i) by A33, A50, A56, FINSEQ_4:15;
hence |.((h1 /. i) - (h1 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A39, A64, JGRAPH_1:28; ::_thesis: verum
end;
A65: for i being Element of NAT st i in dom h1 holds
( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom h1 implies ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) )
assume A66: i in dom h1 ; ::_thesis: ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 )
then h1 . i = f . (h . i) by A21;
then A67: h1 /. i = f . (h . i) by A66, PARTFUN1:def_6;
i in dom h by A20, A66, FINSEQ_3:29;
then A68: h . i in rng h by FUNCT_1:def_3;
dom f = the carrier of I[01] by FUNCT_2:def_1;
then h1 /. i in rng f by A17, A67, A68, FUNCT_1:def_3;
hence ( q1 `2 <= (h1 /. i) `2 & (h1 /. i) `2 <= q2 `2 ) by A3, A7; ::_thesis: verum
end;
for i being Element of NAT st i in dom (Y_axis h1) holds
( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom (Y_axis h1) implies ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) )
assume i in dom (Y_axis h1) ; ::_thesis: ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 )
then i in Seg (len (Y_axis h1)) by FINSEQ_1:def_3;
then i in Seg (len h1) by A28, JGRAPH_1:42;
then A69: i in dom h1 by FINSEQ_1:def_3;
then (Y_axis h1) . i = (h1 /. i) `2 by JGRAPH_1:43;
hence ( q1 `2 <= (Y_axis h1) . i & (Y_axis h1) . i <= q2 `2 ) by A65, A69; ::_thesis: verum
end;
then A70: Y_axis h1 lies_between q1 `2 ,q2 `2 by GOBOARD4:def_2;
A71: f . 1 = p2 by BORSUK_2:def_4;
A72: for i being Element of NAT st i in dom h1 holds
( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )
proof
len h in dom h19 by A20, A28, FINSEQ_3:25;
then h1 . (len h1) = f . (h . (len h)) by A20, A21;
then A73: h1 /. (len h1) = f . (h . (len h)) by A28, FINSEQ_4:15;
1 in dom h19 by A28, FINSEQ_3:25;
then h1 . 1 = f . (h . 1) by A21;
then A74: h1 /. 1 = f . (h . 1) by A28, FINSEQ_4:15;
let i be Element of NAT ; ::_thesis: ( i in dom h1 implies ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) )
assume A75: i in dom h1 ; ::_thesis: ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 )
then h1 . i = f . (h . i) by A21;
then A76: h1 /. i = f . (h . i) by A75, PARTFUN1:def_6;
i in dom h by A20, A75, FINSEQ_3:29;
then A77: h . i in rng h by FUNCT_1:def_3;
dom f = the carrier of I[01] by FUNCT_2:def_1;
then h1 /. i in rng f by A17, A76, A77, FUNCT_1:def_3;
hence ( (h1 /. 1) `1 <= (h1 /. i) `1 & (h1 /. i) `1 <= (h1 /. (len h1)) `1 ) by A3, A5, A30, A71, A14, A15, A74, A73; ::_thesis: verum
end;
for i being Element of NAT st i in dom (X_axis h1) holds
( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom (X_axis h1) implies ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) )
A78: ( (X_axis h1) . 1 = (h1 /. 1) `1 & (X_axis h1) . (len h1) = (h1 /. (len h1)) `1 ) by A28, JGRAPH_1:41;
assume i in dom (X_axis h1) ; ::_thesis: ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) )
then i in Seg (len (X_axis h1)) by FINSEQ_1:def_3;
then i in Seg (len h1) by A28, JGRAPH_1:41;
then A79: i in dom h1 by FINSEQ_1:def_3;
then (X_axis h1) . i = (h1 /. i) `1 by JGRAPH_1:43;
hence ( (X_axis h1) . 1 <= (X_axis h1) . i & (X_axis h1) . i <= (X_axis h1) . (len h1) ) by A72, A79, A78; ::_thesis: verum
end;
then X_axis h1 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) by GOBOARD4:def_2;
then consider f2 being FinSequence of (TOP-REAL 2) such that
A80: f2 is special and
A81: f2 . 1 = h1 . 1 and
A82: f2 . (len f2) = h1 . (len h1) and
A83: len f2 >= len h1 and
A84: ( X_axis f2 lies_between (X_axis h1) . 1,(X_axis h1) . (len h1) & Y_axis f2 lies_between q1 `2 ,q2 `2 ) and
A85: for j being Element of NAT st j in dom f2 holds
ex k being Element of NAT st
( k in dom h1 & |.((f2 /. j) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and
A86: for j being Element of NAT st 1 <= j & j + 1 <= len f2 holds
|.((f2 /. j) - (f2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A13, A31, A28, A70, JGRAPH_1:39;
A87: len f2 >= 1 by A28, A83, XXREAL_0:2;
then A88: f2 . (len f2) = f2 /. (len f2) by FINSEQ_4:15;
consider hb being FinSequence of REAL such that
A89: hb . 1 = 0 and
A90: hb . (len hb) = 1 and
A91: 5 <= len hb and
A92: rng hb c= the carrier of I[01] and
A93: hb is increasing and
A94: for i being Element of NAT
for R being Subset of I[01]
for W being Subset of (Euclid 2) st 1 <= i & i < len hb & R = [.(hb /. i),(hb /. (i + 1)).] & W = g .: R holds
diameter W < (min_dist_min (P9,Q9)) / 5 by A13, Th1;
deffunc H2( Nat) -> set = g . (hb . $1);
ex h29 being FinSequence st
( len h29 = len hb & ( for i being Nat st i in dom h29 holds
h29 . i = H2(i) ) ) from FINSEQ_1:sch_2();
then consider h29 being FinSequence such that
A95: len h29 = len hb and
A96: for i being Nat st i in dom h29 holds
h29 . i = g . (hb . i) ;
rng h29 c= the carrier of (TOP-REAL 2)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h29 or y in the carrier of (TOP-REAL 2) )
A97: dom g = the carrier of I[01] by FUNCT_2:def_1;
assume y in rng h29 ; ::_thesis: y in the carrier of (TOP-REAL 2)
then consider x being set such that
A98: x in dom h29 and
A99: y = h29 . x by FUNCT_1:def_3;
reconsider i = x as Element of NAT by A98;
dom h29 = Seg (len h29) by FINSEQ_1:def_3;
then i in dom hb by A95, A98, FINSEQ_1:def_3;
then A100: hb . i in rng hb by FUNCT_1:def_3;
h29 . i = g . (hb . i) by A96, A98;
then h29 . i in rng g by A92, A100, A97, FUNCT_1:def_3;
hence y in the carrier of (TOP-REAL 2) by A99; ::_thesis: verum
end;
then reconsider h2 = h29 as FinSequence of (TOP-REAL 2) by FINSEQ_1:def_4;
A101: len h2 >= 1 by A91, A95, XXREAL_0:2;
1 in dom h19 by A20, A22, FINSEQ_3:25;
then A102: h1 /. 1 = f . (h . 1) by A21, A29;
A103: 0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def_1;
then A104: p1 in P9 by A3, A30, FUNCT_1:def_3;
A105: 1 <= len hb by A91, XXREAL_0:2;
then A106: h2 . (len h2) = h2 /. (len h2) by A95, FINSEQ_4:15;
A107: g . 0 = q1 by BORSUK_2:def_4;
A108: for i being Element of NAT st 1 <= i & i + 1 <= len h2 holds
|.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
proof
reconsider Qa = Q as Subset of (TOP-REAL 2) ;
A109: dom g = the carrier of I[01] by FUNCT_2:def_1;
reconsider W1 = Q as Subset of (Euclid 2) by TOPREAL3:8;
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len h2 implies |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 )
assume that
A110: 1 <= i and
A111: i + 1 <= len h2 ; ::_thesis: |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5
A112: i < len h2 by A111, NAT_1:13;
then A113: hb . i = hb /. i by A95, A110, FINSEQ_4:15;
A114: 1 < i + 1 by A110, NAT_1:13;
then i + 1 in Seg (len hb) by A95, A111, FINSEQ_1:1;
then i + 1 in dom hb by FINSEQ_1:def_3;
then A115: hb . (i + 1) in rng hb by FUNCT_1:def_3;
A116: i + 1 in dom h29 by A111, A114, FINSEQ_3:25;
then h29 . (i + 1) = g . (hb . (i + 1)) by A96;
then h29 . (i + 1) in rng g by A92, A109, A115, FUNCT_1:def_3;
then A117: g . (hb . (i + 1)) is Element of (TOP-REAL 2) by A96, A116;
i in dom h29 by A110, A112, FINSEQ_3:25;
then A118: h29 . i = g . (hb . i) by A96;
( [#] I[01] is compact & g .: the carrier of I[01] = rng g ) by COMPTS_1:1, RELSET_1:22;
then A119: Qa is compact by A4, WEIERSTR:8;
reconsider Qa = Qa as non empty Subset of (TOP-REAL 2) ;
set r1 = (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1;
A120: hb . (i + 1) = hb /. (i + 1) by A95, A111, A114, FINSEQ_4:15;
A121: for x, y being Point of (Euclid 2) st x in W1 & y in W1 holds
dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
proof
let x, y be Point of (Euclid 2); ::_thesis: ( x in W1 & y in W1 implies dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 )
assume that
A122: x in W1 and
A123: y in W1 ; ::_thesis: dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1
reconsider pw1 = x, pw2 = y as Point of (TOP-REAL 2) by A122, A123;
A124: ( S-bound Qa <= pw2 `2 & pw2 `2 <= N-bound Qa ) by A119, A123, PSCOMP_1:24;
( S-bound Qa <= pw1 `2 & pw1 `2 <= N-bound Qa ) by A119, A122, PSCOMP_1:24;
then A125: abs ((pw1 `2) - (pw2 `2)) <= (N-bound Qa) - (S-bound Qa) by A124, JGRAPH_1:27;
A126: ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by XREAL_1:29;
A127: ( W-bound Qa <= pw2 `1 & pw2 `1 <= E-bound Qa ) by A119, A123, PSCOMP_1:24;
( W-bound Qa <= pw1 `1 & pw1 `1 <= E-bound Qa ) by A119, A122, PSCOMP_1:24;
then abs ((pw1 `1) - (pw2 `1)) <= (E-bound Qa) - (W-bound Qa) by A127, JGRAPH_1:27;
then (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= ((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa)) by A125, XREAL_1:7;
then A128: (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A126, XXREAL_0:2;
( dist (x,y) = |.(pw1 - pw2).| & |.(pw1 - pw2).| <= (abs ((pw1 `1) - (pw2 `1))) + (abs ((pw1 `2) - (pw2 `2))) ) by JGRAPH_1:28, JGRAPH_1:32;
hence dist (x,y) <= (((E-bound Qa) - (W-bound Qa)) + ((N-bound Qa) - (S-bound Qa))) + 1 by A128, XXREAL_0:2; ::_thesis: verum
end;
0 in the carrier of I[01] by BORSUK_1:43;
then A129: g . 0 in rng g by A109, FUNCT_1:def_3;
then ( S-bound Qa <= q1 `2 & q1 `2 <= N-bound Qa ) by A4, A107, A119, PSCOMP_1:24;
then S-bound Qa <= N-bound Qa by XXREAL_0:2;
then A130: 0 <= (N-bound Qa) - (S-bound Qa) by XREAL_1:48;
i in Seg (len hb) by A95, A110, A112, FINSEQ_1:1;
then A131: i in dom hb by FINSEQ_1:def_3;
then A132: hb . i in rng hb by FUNCT_1:def_3;
then h29 . i in rng g by A92, A118, A109, FUNCT_1:def_3;
then reconsider w1 = g . (hb . i), w2 = g . (hb . (i + 1)) as Point of (Euclid 2) by A118, A117, TOPREAL3:8;
i + 1 in Seg (len hb) by A95, A111, A114, FINSEQ_1:1;
then A133: i + 1 in dom hb by FINSEQ_1:def_3;
then hb . (i + 1) in rng hb by FUNCT_1:def_3;
then reconsider R = [.(hb /. i),(hb /. (i + 1)).] as Subset of I[01] by A92, A132, A113, A120, BORSUK_1:40, XXREAL_2:def_12;
i < i + 1 by NAT_1:13;
then A134: hb /. i <= hb /. (i + 1) by A93, A131, A113, A133, A120, SEQM_3:def_1;
then hb . i in R by A113, XXREAL_1:1;
then A135: w1 in g .: R by A109, FUNCT_1:def_6;
( W-bound Qa <= q1 `1 & q1 `1 <= E-bound Qa ) by A4, A107, A119, A129, PSCOMP_1:24;
then W-bound Qa <= E-bound Qa by XXREAL_0:2;
then 0 <= (E-bound Qa) - (W-bound Qa) by XREAL_1:48;
then A136: W1 is bounded by A130, A121, TBSP_1:def_7;
hb . (i + 1) in R by A120, A134, XXREAL_1:1;
then A137: w2 in g .: R by A109, FUNCT_1:def_6;
reconsider W = g .: R as Subset of (Euclid 2) by TOPREAL3:8;
dom g = [#] I[01] by FUNCT_2:def_1;
then Q = g .: [.0,1.] by A4, BORSUK_1:40, RELAT_1:113;
then W is bounded by A136, BORSUK_1:40, RELAT_1:123, TBSP_1:14;
then A138: dist (w1,w2) <= diameter W by A135, A137, TBSP_1:def_8;
diameter W < (min_dist_min (P9,Q9)) / 5 by A94, A95, A110, A112;
then A139: dist (w1,w2) < (min_dist_min (P9,Q9)) / 5 by A138, XXREAL_0:2;
h2 . (i + 1) = h2 /. (i + 1) by A111, A114, FINSEQ_4:15;
then A140: h2 /. (i + 1) = g . (hb . (i + 1)) by A96, A116;
h2 /. i = g . (hb . i) by A110, A112, A118, FINSEQ_4:15;
hence |.((h2 /. i) - (h2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A140, A139, JGRAPH_1:28; ::_thesis: verum
end;
A141: dom hb = Seg (len hb) by FINSEQ_1:def_3;
A142: for i being Element of NAT st i in dom hb holds
h2 /. i = g . (hb . i)
proof
let i be Element of NAT ; ::_thesis: ( i in dom hb implies h2 /. i = g . (hb . i) )
assume A143: i in dom hb ; ::_thesis: h2 /. i = g . (hb . i)
then i in dom h29 by A95, FINSEQ_3:29;
then A144: h2 . i = g . (hb . i) by A96;
( 1 <= i & i <= len hb ) by A141, A143, FINSEQ_1:1;
hence h2 /. i = g . (hb . i) by A95, A144, FINSEQ_4:15; ::_thesis: verum
end;
A145: for i being Element of NAT st i in dom h2 holds
( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom h2 implies ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) )
assume i in dom h2 ; ::_thesis: ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 )
then i in Seg (len h2) by FINSEQ_1:def_3;
then i in dom hb by A95, FINSEQ_1:def_3;
then A146: ( h2 /. i = g . (hb . i) & hb . i in rng hb ) by A142, FUNCT_1:def_3;
dom g = the carrier of I[01] by FUNCT_2:def_1;
then h2 /. i in rng g by A92, A146, FUNCT_1:def_3;
hence ( p1 `1 <= (h2 /. i) `1 & (h2 /. i) `1 <= p2 `1 ) by A4, A6; ::_thesis: verum
end;
for i being Element of NAT st i in dom (X_axis h2) holds
( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom (X_axis h2) implies ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) )
assume i in dom (X_axis h2) ; ::_thesis: ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 )
then i in Seg (len (X_axis h2)) by FINSEQ_1:def_3;
then i in Seg (len h2) by A101, JGRAPH_1:41;
then A147: i in dom h2 by FINSEQ_1:def_3;
then (X_axis h2) . i = (h2 /. i) `1 by JGRAPH_1:43;
hence ( p1 `1 <= (X_axis h2) . i & (X_axis h2) . i <= p2 `1 ) by A145, A147; ::_thesis: verum
end;
then A148: X_axis h2 lies_between p1 `1 ,p2 `1 by GOBOARD4:def_2;
A149: g . 1 = q2 by BORSUK_2:def_4;
A150: for i being Element of NAT st i in dom h2 holds
( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )
proof
let i be Element of NAT ; ::_thesis: ( i in dom h2 implies ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) )
assume i in dom h2 ; ::_thesis: ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 )
then i in Seg (len h2) by FINSEQ_1:def_3;
then i in dom hb by A95, FINSEQ_1:def_3;
then A151: ( h2 /. i = g . (hb . i) & hb . i in rng hb ) by A142, FUNCT_1:def_3;
1 in Seg (len hb) by A95, A101, FINSEQ_1:1;
then 1 in dom hb by FINSEQ_1:def_3;
then A152: h2 /. 1 = g . (hb . 1) by A142;
len hb in Seg (len hb) by A95, A101, FINSEQ_1:1;
then len hb in dom hb by FINSEQ_1:def_3;
then A153: h2 /. (len h2) = g . (hb . (len hb)) by A95, A142;
dom g = the carrier of I[01] by FUNCT_2:def_1;
then h2 /. i in rng g by A92, A151, FUNCT_1:def_3;
hence ( (h2 /. 1) `2 <= (h2 /. i) `2 & (h2 /. i) `2 <= (h2 /. (len h2)) `2 ) by A4, A8, A107, A149, A89, A90, A152, A153; ::_thesis: verum
end;
for i being Element of NAT st i in dom (Y_axis h2) holds
( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )
proof
let i be Element of NAT ; ::_thesis: ( i in dom (Y_axis h2) implies ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) )
A154: ( (Y_axis h2) . 1 = (h2 /. 1) `2 & (Y_axis h2) . (len h2) = (h2 /. (len h2)) `2 ) by A101, JGRAPH_1:42;
assume i in dom (Y_axis h2) ; ::_thesis: ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) )
then i in Seg (len (Y_axis h2)) by FINSEQ_1:def_3;
then i in Seg (len h2) by A101, JGRAPH_1:42;
then A155: i in dom h2 by FINSEQ_1:def_3;
then (Y_axis h2) . i = (h2 /. i) `2 by JGRAPH_1:43;
hence ( (Y_axis h2) . 1 <= (Y_axis h2) . i & (Y_axis h2) . i <= (Y_axis h2) . (len h2) ) by A150, A155, A154; ::_thesis: verum
end;
then Y_axis h2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) by GOBOARD4:def_2;
then consider g2 being FinSequence of (TOP-REAL 2) such that
A156: g2 is special and
A157: g2 . 1 = h2 . 1 and
A158: g2 . (len g2) = h2 . (len h2) and
A159: len g2 >= len h2 and
A160: ( Y_axis g2 lies_between (Y_axis h2) . 1,(Y_axis h2) . (len h2) & X_axis g2 lies_between p1 `1 ,p2 `1 ) and
A161: for j being Element of NAT st j in dom g2 holds
ex k being Element of NAT st
( k in dom h2 & |.((g2 /. j) - (h2 /. k)).| < (min_dist_min (P9,Q9)) / 5 ) and
A162: for j being Element of NAT st 1 <= j & j + 1 <= len g2 holds
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A13, A101, A148, A108, JGRAPH_1:40;
A163: len g2 >= 1 by A101, A159, XXREAL_0:2;
then A164: g2 /. (len g2) = g2 . (len g2) by FINSEQ_4:15;
1 in dom hb by A105, FINSEQ_3:25;
then A165: h2 /. 1 = q1 by A107, A89, A142;
A166: h2 . 1 = h2 /. 1 by A105, A95, FINSEQ_4:15;
A167: h1 . (len h1) = h1 /. (len h1) by A28, FINSEQ_4:15;
then A168: (X_axis f2) . (len f2) = (h1 /. (len h1)) `1 by A82, A87, A88, JGRAPH_1:41
.= (X_axis h1) . (len h1) by A28, JGRAPH_1:41 ;
len h in dom h19 by A20, A28, FINSEQ_3:25;
then h1 /. (len h1) = p2 by A71, A15, A20, A21, A167;
then A169: (X_axis f2) . (len f2) = p2 `1 by A82, A87, A167, A88, JGRAPH_1:41;
5 <= len f2 by A16, A20, A83, XXREAL_0:2;
then A170: 2 <= len f2 by XXREAL_0:2;
0 in dom g by A103, FUNCT_2:def_1;
then A171: q1 in Q9 by A4, A107, FUNCT_1:def_3;
A172: f2 . 1 = f2 /. 1 by A87, FINSEQ_4:15;
g2 . 1 = g2 /. 1 by A163, FINSEQ_4:15;
then A173: (Y_axis g2) . 1 = (h2 /. 1) `2 by A157, A163, A166, JGRAPH_1:42
.= (Y_axis h2) . 1 by A101, JGRAPH_1:42 ;
g2 /. 1 = g2 . 1 by A163, FINSEQ_4:15;
then A174: (Y_axis g2) . 1 = q1 `2 by A157, A163, A165, A166, JGRAPH_1:42;
len hb in dom hb by A105, FINSEQ_3:25;
then g2 . (len g2) = q2 by A149, A90, A95, A142, A158, A106;
then A175: (Y_axis g2) . (len g2) = q2 `2 by A163, A164, JGRAPH_1:42;
g2 . (len g2) = g2 /. (len g2) by A163, FINSEQ_4:15;
then A176: (Y_axis g2) . (len g2) = (h2 /. (len h2)) `2 by A158, A163, A106, JGRAPH_1:42
.= (Y_axis h2) . (len h2) by A101, JGRAPH_1:42 ;
5 <= len g2 by A91, A95, A159, XXREAL_0:2;
then A177: 2 <= len g2 by XXREAL_0:2;
1 in dom h19 by A28, FINSEQ_3:25;
then h1 . 1 = f . (h . 1) by A21;
then A178: (X_axis f2) . 1 = p1 `1 by A30, A14, A81, A87, A172, JGRAPH_1:41;
A179: (X_axis f2) . 1 = (h1 /. 1) `1 by A81, A87, A29, A172, JGRAPH_1:41
.= (X_axis h1) . 1 by A28, JGRAPH_1:41 ;
now__::_thesis:_(_(_p1_=_p2_&_contradiction_)_or_(_p1_<>_p2_&_contradiction_)_)
percases ( p1 = p2 or p1 <> p2 ) ;
caseA180: p1 = p2 ; ::_thesis: contradiction
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def_1;
then A181: p1 in P by A3, A30, FUNCT_1:3;
0 in the carrier of I[01] by BORSUK_1:43;
then A182: 0 in dom g by FUNCT_2:def_1;
then A183: q1 in Q by A4, A107, FUNCT_1:3;
A184: for q being Point of (TOP-REAL 2) st q in Q holds
q `1 = p1 `1
proof
let q be Point of (TOP-REAL 2); ::_thesis: ( q in Q implies q `1 = p1 `1 )
assume q in Q ; ::_thesis: q `1 = p1 `1
then ( p1 `1 <= q `1 & q `1 <= p2 `1 ) by A6;
hence q `1 = p1 `1 by A180, XXREAL_0:1; ::_thesis: verum
end;
A185: now__::_thesis:_not_q1_`2_=_q2_`2
assume A186: q1 `2 = q2 `2 ; ::_thesis: contradiction
( q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) by A7, A181;
then A187: p1 `2 = q1 `2 by A186, XXREAL_0:1;
q1 `1 = p1 `1 by A4, A107, A184, A182, FUNCT_1:3;
then q1 = p1 by A187, TOPREAL3:6;
hence contradiction by A11, A183, A181, XBOOLE_0:def_4; ::_thesis: verum
end;
A188: p1 in LSeg (q1,q2)
proof
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def_1;
then g . 1 in rng g by FUNCT_1:3;
then ( p1 `1 <= q2 `1 & q2 `1 <= p2 `1 ) by A4, A6, A149;
then A189: p1 `1 = q2 `1 by A180, XXREAL_0:1;
set ln = ((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2));
A190: (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2) = (((p1 `2) - (q1 `2)) * (q2 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74
.= (((p1 `2) * (q2 `2)) - ((q1 `2) * (q2 `2))) / ((q2 `2) - (q1 `2)) ;
A191: (q2 `2) - (q1 `2) <> 0 by A185;
then 1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) = (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:60
.= (((q2 `2) - (q1 `2)) - ((p1 `2) - (q1 `2))) / ((q2 `2) - (q1 `2)) by XCMPLX_1:120
.= ((q2 `2) - (p1 `2)) / ((q2 `2) - (q1 `2)) ;
then A192: (1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2) = (((q2 `2) - (p1 `2)) * (q1 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74
.= (((q2 `2) * (q1 `2)) - ((p1 `2) * (q1 `2))) / ((q2 `2) - (q1 `2)) ;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def_1;
then q1 in Q by A4, A107, FUNCT_1:3;
then ( p1 `1 <= q1 `1 & q1 `1 <= p2 `1 ) by A6;
then A193: p1 `1 = q1 `1 by A180, XXREAL_0:1;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def_1;
then A194: f . 0 in rng f by FUNCT_1:3;
then A195: q1 `2 <= p1 `2 by A3, A7, A30;
A196: (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `1 = (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `1) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:2
.= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `1)) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:4
.= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (p1 `1)) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (p1 `1)) by A193, A189, TOPREAL3:4
.= p1 `1 ;
(((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `2 = (((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `2) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:2
.= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + (((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:4
.= ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2)) by TOPREAL3:4
.= ((((q2 `2) * (q1 `2)) - ((p1 `2) * (q1 `2))) + (((p1 `2) * (q2 `2)) - ((q1 `2) * (q2 `2)))) / ((q2 `2) - (q1 `2)) by A192, A190, XCMPLX_1:62
.= ((p1 `2) * ((q2 `2) - (q1 `2))) / ((q2 `2) - (q1 `2))
.= (p1 `2) * (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:74
.= (p1 `2) * 1 by A191, XCMPLX_1:60
.= p1 `2 ;
then A197: ((1 - (((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) = p1 by A196, TOPREAL3:6;
A198: p1 `2 <= q2 `2 by A3, A7, A30, A194;
then q2 `2 >= q1 `2 by A195, XXREAL_0:2;
then q2 `2 > q1 `2 by A185, XXREAL_0:1;
then A199: (q2 `2) - (q1 `2) > 0 by XREAL_1:50;
(p1 `2) - (q1 `2) <= (q2 `2) - (q1 `2) by A198, XREAL_1:13;
then ((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= ((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) by A199, XREAL_1:72;
then A200: ((p1 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= 1 by A199, XCMPLX_1:60;
(p1 `2) - (q1 `2) >= 0 by A195, XREAL_1:48;
hence p1 in LSeg (q1,q2) by A199, A200, A197; ::_thesis: verum
end;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def_1;
then A201: q2 in Q by A4, A149, FUNCT_1:3;
Q c= LSeg (q1,q2)
proof
( p1 `1 <= q2 `1 & q2 `1 <= p2 `1 ) by A6, A201;
then A202: p1 `1 = q2 `1 by A180, XXREAL_0:1;
( p1 `1 <= q1 `1 & q1 `1 <= p2 `1 ) by A6, A183;
then A203: p1 `1 = q1 `1 by A180, XXREAL_0:1;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Q or z in LSeg (q1,q2) )
assume A204: z in Q ; ::_thesis: z in LSeg (q1,q2)
then reconsider qz = z as Point of (TOP-REAL 2) ;
A205: qz `2 <= q2 `2 by A8, A204;
set ln = ((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2));
A206: (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2) = (((qz `2) - (q1 `2)) * (q2 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74
.= (((qz `2) * (q2 `2)) - ((q1 `2) * (q2 `2))) / ((q2 `2) - (q1 `2)) ;
A207: (q2 `2) - (q1 `2) <> 0 by A185;
then 1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) = (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:60
.= (((q2 `2) - (q1 `2)) - ((qz `2) - (q1 `2))) / ((q2 `2) - (q1 `2)) by XCMPLX_1:120
.= ((q2 `2) - (qz `2)) / ((q2 `2) - (q1 `2)) ;
then A208: (1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2) = (((q2 `2) - (qz `2)) * (q1 `2)) / ((q2 `2) - (q1 `2)) by XCMPLX_1:74
.= (((q2 `2) * (q1 `2)) - ((qz `2) * (q1 `2))) / ((q2 `2) - (q1 `2)) ;
A209: (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `2 = (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `2) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:2
.= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `2) by TOPREAL3:4
.= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `2)) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (q2 `2)) by TOPREAL3:4
.= ((((q2 `2) * (q1 `2)) - ((qz `2) * (q1 `2))) + (((qz `2) * (q2 `2)) - ((q1 `2) * (q2 `2)))) / ((q2 `2) - (q1 `2)) by A208, A206, XCMPLX_1:62
.= ((qz `2) * ((q2 `2) - (q1 `2))) / ((q2 `2) - (q1 `2))
.= (qz `2) * (((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) by XCMPLX_1:74
.= (qz `2) * 1 by A207, XCMPLX_1:60
.= qz `2 ;
A210: ( p1 `1 <= qz `1 & qz `1 <= p2 `1 ) by A6, A204;
(((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2)) `1 = (((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) `1) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:2
.= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (q1 `1)) + (((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) `1) by TOPREAL3:4
.= ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * (p1 `1)) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * (p1 `1)) by A203, A202, TOPREAL3:4
.= qz `1 by A180, A210, XXREAL_0:1 ;
then A211: ((1 - (((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)))) * q1) + ((((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2))) * q2) = qz by A209, TOPREAL3:6;
A212: q1 `2 <= qz `2 by A8, A204;
then q2 `2 >= q1 `2 by A205, XXREAL_0:2;
then q2 `2 > q1 `2 by A185, XXREAL_0:1;
then A213: (q2 `2) - (q1 `2) > 0 by XREAL_1:50;
(qz `2) - (q1 `2) <= (q2 `2) - (q1 `2) by A205, XREAL_1:13;
then ((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= ((q2 `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) by A213, XREAL_1:72;
then A214: ((qz `2) - (q1 `2)) / ((q2 `2) - (q1 `2)) <= 1 by A213, XCMPLX_1:60;
(qz `2) - (q1 `2) >= 0 by A212, XREAL_1:48;
hence z in LSeg (q1,q2) by A213, A214, A211; ::_thesis: verum
end;
then p1 in Q by A4, A188, Th3;
hence contradiction by A104, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
caseA215: p1 <> p2 ; ::_thesis: contradiction
A216: 1 <= len hb by A91, XXREAL_0:2;
then 1 in dom hb by FINSEQ_3:25;
then A217: h2 /. 1 = g . (hb . 1) by A142;
A218: now__::_thesis:_not_q1_=_q2
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def_1;
then A219: q1 in Q by A4, A107, FUNCT_1:3;
0 in the carrier of I[01] by BORSUK_1:43;
then A220: 0 in dom f by FUNCT_2:def_1;
then A221: p1 in P by A3, A30, FUNCT_1:3;
assume A222: q1 = q2 ; ::_thesis: contradiction
A223: for p being Point of (TOP-REAL 2) st p in P holds
p `2 = q1 `2
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in P implies p `2 = q1 `2 )
assume p in P ; ::_thesis: p `2 = q1 `2
then ( q1 `2 <= p `2 & p `2 <= q2 `2 ) by A7;
hence p `2 = q1 `2 by A222, XXREAL_0:1; ::_thesis: verum
end;
A224: now__::_thesis:_not_p1_`1_=_p2_`1
assume A225: p1 `1 = p2 `1 ; ::_thesis: contradiction
( p1 `1 <= q1 `1 & q1 `1 <= p2 `1 ) by A6, A219;
then A226: q1 `1 = p1 `1 by A225, XXREAL_0:1;
p1 `2 = q1 `2 by A3, A30, A223, A220, FUNCT_1:3;
then p1 = q1 by A226, TOPREAL3:6;
hence contradiction by A11, A221, A219, XBOOLE_0:def_4; ::_thesis: verum
end;
A227: q1 in LSeg (p1,p2)
proof
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom f by FUNCT_2:def_1;
then f . 1 in rng f by FUNCT_1:3;
then ( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A3, A7, A71;
then A228: q1 `2 = p2 `2 by A222, XXREAL_0:1;
set ln = ((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1));
A229: (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1) = (((q1 `1) - (p1 `1)) * (p2 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74
.= (((q1 `1) * (p2 `1)) - ((p1 `1) * (p2 `1))) / ((p2 `1) - (p1 `1)) ;
A230: (p2 `1) - (p1 `1) <> 0 by A224;
then 1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) = (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:60
.= (((p2 `1) - (p1 `1)) - ((q1 `1) - (p1 `1))) / ((p2 `1) - (p1 `1)) by XCMPLX_1:120
.= ((p2 `1) - (q1 `1)) / ((p2 `1) - (p1 `1)) ;
then A231: (1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1) = (((p2 `1) - (q1 `1)) * (p1 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74
.= (((p2 `1) * (p1 `1)) - ((q1 `1) * (p1 `1))) / ((p2 `1) - (p1 `1)) ;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def_1;
then f . 0 in rng f by FUNCT_1:3;
then ( q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) by A3, A7, A30;
then A232: q1 `2 = p1 `2 by A222, XXREAL_0:1;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def_1;
then A233: g . 0 in rng g by FUNCT_1:3;
then A234: p1 `1 <= q1 `1 by A4, A6, A107;
A235: (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `2 = (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `2) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:2
.= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `2)) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:4
.= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (q1 `2)) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (q1 `2)) by A232, A228, TOPREAL3:4 ;
(((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `1 = (((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `1) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:2
.= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + (((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:4
.= ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1)) by TOPREAL3:4
.= ((((p2 `1) * (p1 `1)) - ((q1 `1) * (p1 `1))) + (((q1 `1) * (p2 `1)) - ((p1 `1) * (p2 `1)))) / ((p2 `1) - (p1 `1)) by A231, A229, XCMPLX_1:62
.= ((q1 `1) * ((p2 `1) - (p1 `1))) / ((p2 `1) - (p1 `1))
.= (q1 `1) * (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:74
.= (q1 `1) * 1 by A230, XCMPLX_1:60 ;
then A236: ((1 - (((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) = q1 by A235, TOPREAL3:6;
A237: q1 `1 <= p2 `1 by A4, A6, A107, A233;
then p2 `1 >= p1 `1 by A234, XXREAL_0:2;
then p2 `1 > p1 `1 by A224, XXREAL_0:1;
then A238: (p2 `1) - (p1 `1) > 0 by XREAL_1:50;
(q1 `1) - (p1 `1) <= (p2 `1) - (p1 `1) by A237, XREAL_1:13;
then ((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= ((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) by A238, XREAL_1:72;
then A239: ((q1 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1 by A238, XCMPLX_1:60;
(q1 `1) - (p1 `1) >= 0 by A234, XREAL_1:48;
hence q1 in LSeg (p1,p2) by A238, A239, A236; ::_thesis: verum
end;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom f by FUNCT_2:def_1;
then A240: p2 in P by A3, A71, FUNCT_1:3;
P c= LSeg (p1,p2)
proof
( q1 `2 <= p2 `2 & p2 `2 <= q2 `2 ) by A7, A240;
then A241: q1 `2 = p2 `2 by A222, XXREAL_0:1;
( q1 `2 <= p1 `2 & p1 `2 <= q2 `2 ) by A7, A221;
then A242: q1 `2 = p1 `2 by A222, XXREAL_0:1;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in P or z in LSeg (p1,p2) )
assume A243: z in P ; ::_thesis: z in LSeg (p1,p2)
then reconsider pz = z as Point of (TOP-REAL 2) ;
A244: pz `1 <= p2 `1 by A5, A243;
set ln = ((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1));
A245: (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1) = (((pz `1) - (p1 `1)) * (p2 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74
.= (((pz `1) * (p2 `1)) - ((p1 `1) * (p2 `1))) / ((p2 `1) - (p1 `1)) ;
A246: (p2 `1) - (p1 `1) <> 0 by A224;
then 1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) = (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:60
.= (((p2 `1) - (p1 `1)) - ((pz `1) - (p1 `1))) / ((p2 `1) - (p1 `1)) by XCMPLX_1:120
.= ((p2 `1) - (pz `1)) / ((p2 `1) - (p1 `1)) ;
then A247: (1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1) = (((p2 `1) - (pz `1)) * (p1 `1)) / ((p2 `1) - (p1 `1)) by XCMPLX_1:74
.= (((p2 `1) * (p1 `1)) - ((pz `1) * (p1 `1))) / ((p2 `1) - (p1 `1)) ;
A248: (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `1 = (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `1) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:2
.= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `1) by TOPREAL3:4
.= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `1)) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (p2 `1)) by TOPREAL3:4
.= ((((p2 `1) * (p1 `1)) - ((pz `1) * (p1 `1))) + (((pz `1) * (p2 `1)) - ((p1 `1) * (p2 `1)))) / ((p2 `1) - (p1 `1)) by A247, A245, XCMPLX_1:62
.= ((pz `1) * ((p2 `1) - (p1 `1))) / ((p2 `1) - (p1 `1))
.= (pz `1) * (((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) by XCMPLX_1:74
.= (pz `1) * 1 by A246, XCMPLX_1:60
.= pz `1 ;
A249: ( q1 `2 <= pz `2 & pz `2 <= q2 `2 ) by A7, A243;
(((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2)) `2 = (((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) `2) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:2
.= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (p1 `2)) + (((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) `2) by TOPREAL3:4
.= ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * (q1 `2)) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * (q1 `2)) by A242, A241, TOPREAL3:4
.= pz `2 by A222, A249, XXREAL_0:1 ;
then A250: ((1 - (((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)))) * p1) + ((((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1))) * p2) = pz by A248, TOPREAL3:6;
A251: p1 `1 <= pz `1 by A5, A243;
then p2 `1 >= p1 `1 by A244, XXREAL_0:2;
then p2 `1 > p1 `1 by A224, XXREAL_0:1;
then A252: (p2 `1) - (p1 `1) > 0 by XREAL_1:50;
(pz `1) - (p1 `1) <= (p2 `1) - (p1 `1) by A244, XREAL_1:13;
then ((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= ((p2 `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) by A252, XREAL_1:72;
then A253: ((pz `1) - (p1 `1)) / ((p2 `1) - (p1 `1)) <= 1 by A252, XCMPLX_1:60;
(pz `1) - (p1 `1) >= 0 by A251, XREAL_1:48;
hence z in LSeg (p1,p2) by A252, A253, A250; ::_thesis: verum
end;
then q1 in P by A3, A227, Th3;
hence contradiction by A171, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
len hb in dom hb by A216, FINSEQ_3:25;
then A254: g2 . 1 <> g2 . (len g2) by A107, A149, A89, A90, A95, A142, A157, A158, A166, A106, A218, A217;
f2 /. 1 <> f2 /. (len f2) by A30, A71, A14, A15, A20, A21, A81, A82, A29, A172, A88, A102, A23, A215;
then L~ f2 meets L~ g2 by A80, A84, A156, A160, A172, A88, A178, A169, A174, A175, A179, A168, A173, A176, A170, A177, A254, JGRAPH_1:26;
then consider s being set such that
A255: s in L~ f2 and
A256: s in L~ g2 by XBOOLE_0:3;
reconsider ps = s as Point of (TOP-REAL 2) by A255;
ps in union { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A255, TOPREAL1:def_4;
then consider x being set such that
A257: ( ps in x & x in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ) by TARSKI:def_4;
ps in union { (LSeg (g2,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g2 ) } by A256, TOPREAL1:def_4;
then consider y being set such that
A258: ( ps in y & y in { (LSeg (g2,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len g2 ) } ) by TARSKI:def_4;
consider i being Element of NAT such that
A259: x = LSeg (f2,i) and
A260: 1 <= i and
A261: i + 1 <= len f2 by A257;
LSeg (f2,i) = LSeg ((f2 /. i),(f2 /. (i + 1))) by A260, A261, TOPREAL1:def_3;
then A262: |.(ps - (f2 /. i)).| <= |.((f2 /. i) - (f2 /. (i + 1))).| by A257, A259, JGRAPH_1:36;
i < len f2 by A261, NAT_1:13;
then i in dom f2 by A260, FINSEQ_3:25;
then consider k being Element of NAT such that
A263: k in dom h1 and
A264: |.((f2 /. i) - (h1 /. k)).| < (min_dist_min (P9,Q9)) / 5 by A85;
consider j being Element of NAT such that
A265: y = LSeg (g2,j) and
A266: 1 <= j and
A267: j + 1 <= len g2 by A258;
LSeg (g2,j) = LSeg ((g2 /. j),(g2 /. (j + 1))) by A266, A267, TOPREAL1:def_3;
then A268: |.(ps - (g2 /. j)).| <= |.((g2 /. j) - (g2 /. (j + 1))).| by A258, A265, JGRAPH_1:36;
reconsider p11 = h1 /. k as Point of (TOP-REAL 2) ;
|.((f2 /. i) - (f2 /. (i + 1))).| < (min_dist_min (P9,Q9)) / 5 by A86, A260, A261;
then |.(ps - (f2 /. i)).| < (min_dist_min (P9,Q9)) / 5 by A262, XXREAL_0:2;
then ( |.(ps - (h1 /. k)).| <= |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| & |.(ps - (f2 /. i)).| + |.((f2 /. i) - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) ) by A264, TOPRNS_1:34, XREAL_1:8;
then |.(ps - (h1 /. k)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;
then A269: |.(p11 - ps).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by TOPRNS_1:27;
A270: k in Seg (len h1) by A263, FINSEQ_1:def_3;
then ( 1 <= k & k <= len h1 ) by FINSEQ_1:1;
then h1 . k = h1 /. k by FINSEQ_4:15;
then A271: h1 /. k = f . (h . k) by A21, A263;
j < len g2 by A267, NAT_1:13;
then j in dom g2 by A266, FINSEQ_3:25;
then consider k9 being Element of NAT such that
A272: k9 in dom h2 and
A273: |.((g2 /. j) - (h2 /. k9)).| < (min_dist_min (P9,Q9)) / 5 by A161;
k9 in Seg (len h2) by A272, FINSEQ_1:def_3;
then k9 in dom hb by A95, FINSEQ_1:def_3;
then A274: ( hb . k9 in rng hb & h2 /. k9 = g . (hb . k9) ) by A142, FUNCT_1:def_3;
reconsider q11 = h2 /. k9 as Point of (TOP-REAL 2) ;
reconsider x1 = p11, x2 = q11 as Point of (Euclid 2) by EUCLID:22;
dom g = the carrier of I[01] by FUNCT_2:def_1;
then A275: h2 /. k9 in rng g by A92, A274, FUNCT_1:def_3;
k in dom h by A20, A270, FINSEQ_1:def_3;
then A276: h . k in rng h by FUNCT_1:def_3;
dom f = the carrier of I[01] by FUNCT_2:def_1;
then h1 /. k in P by A3, A17, A271, A276, FUNCT_1:def_3;
then min_dist_min (P9,Q9) <= dist (x1,x2) by A4, A10, A9, A275, WEIERSTR:34;
then A277: min_dist_min (P9,Q9) <= |.(p11 - q11).| by JGRAPH_1:28;
|.((g2 /. j) - (g2 /. (j + 1))).| < (min_dist_min (P9,Q9)) / 5 by A162, A266, A267;
then |.(ps - (g2 /. j)).| < (min_dist_min (P9,Q9)) / 5 by A268, XXREAL_0:2;
then ( |.(ps - (h2 /. k9)).| <= |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| & |.(ps - (g2 /. j)).| + |.((g2 /. j) - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) ) by A273, TOPRNS_1:34, XREAL_1:8;
then |.(ps - (h2 /. k9)).| < ((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;
then ( |.(p11 - q11).| <= |.(p11 - ps).| + |.(ps - q11).| & |.(p11 - ps).| + |.(ps - q11).| < (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + (((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) ) by A269, TOPRNS_1:34, XREAL_1:8;
then |.(p11 - q11).| < ((((min_dist_min (P9,Q9)) / 5) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5)) + ((min_dist_min (P9,Q9)) / 5) by XXREAL_0:2;
then min_dist_min (P9,Q9) < 4 * ((min_dist_min (P9,Q9)) / 5) by A277, XXREAL_0:2;
then (4 * ((min_dist_min (P9,Q9)) / 5)) - (5 * ((min_dist_min (P9,Q9)) / 5)) > 0 by XREAL_1:50;
then ((4 - 5) * ((min_dist_min (P9,Q9)) / 5)) / ((min_dist_min (P9,Q9)) / 5) > 0 by A13, XREAL_1:139;
then 4 - 5 > 0 by A12;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th5: :: JGRAPH_8:5
for a, b, c, d being real number
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
proof
let a, b, c, d be real number ; ::_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 set 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 set 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 set 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 set 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
end;
theorem :: JGRAPH_8:6
for a, b, c, d being real number
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
proof
let a, b, c, d be real number ; ::_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);
percases ( Trectangle (a,b,c,d) is empty or not Trectangle (a,b,c,d) is empty ) ;
supposeA2: 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 set such that
A8: y in rng f and
A9: y in rng g by XBOOLE_0:3;
consider t being set such that
A10: t in dom g and
A11: g . t = y by A9, FUNCT_1:def_3;
consider s being set 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;
end;