:: JORDAN_A semantic presentation begin theorem Th1: :: JORDAN_A:1 for T being non empty TopSpace for f being continuous RealMap of T for A being compact Subset of T holds f .: A is compact proof let T be non empty TopSpace; ::_thesis: for f being continuous RealMap of T for A being compact Subset of T holds f .: A is compact let f be continuous RealMap of T; ::_thesis: for A being compact Subset of T holds f .: A is compact let A be compact Subset of T; ::_thesis: f .: A is compact reconsider g = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; [#] (g .: A) is compact by WEIERSTR:9, WEIERSTR:13; hence f .: A is compact by WEIERSTR:def_1; ::_thesis: verum end; theorem Th2: :: JORDAN_A:2 for A being compact Subset of REAL for B being non empty Subset of REAL st B c= A holds lower_bound B in A proof let A be compact Subset of REAL; ::_thesis: for B being non empty Subset of REAL st B c= A holds lower_bound B in A let B be non empty Subset of REAL; ::_thesis: ( B c= A implies lower_bound B in A ) assume A1: B c= A ; ::_thesis: lower_bound B in A A2: A is real-bounded by RCOMP_1:10; then A3: B is bounded_below by A1, XXREAL_2:44; A4: Cl B c= A by A1, MEASURE6:57; Cl B is bounded_below by A1, A2, MEASURE6:57, XXREAL_2:44; then lower_bound (Cl B) in Cl B by RCOMP_1:13; then lower_bound (Cl B) in A by A4; hence lower_bound B in A by A3, TOPREAL6:68; ::_thesis: verum end; theorem :: JORDAN_A:3 for n being Element of NAT for A, B being non empty compact Subset of (TOP-REAL n) for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: A) proof let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n) for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: A) let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: A) let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: A) let g be RealMap of (TOP-REAL n); ::_thesis: ( ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: A) ) assume A1: for p being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ; ::_thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: A) A2: [:A,B:] is compact by BORSUK_3:23; then A3: f .: [:A,B:] is compact by Th1; A4: f .: [:A,B:] is real-bounded by A2, Th1, RCOMP_1:10; A5: g .: A c= f .: [:A,B:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in g .: A or u in f .: [:A,B:] ) assume u in g .: A ; ::_thesis: u in f .: [:A,B:] then consider p being Point of (TOP-REAL n) such that A6: p in A and A7: u = g . p by FUNCT_2:65; consider q being Point of (TOP-REAL n) such that A8: q in B by SUBSET_1:4; consider G being Subset of REAL such that A9: G = { (f . (p,q1)) where q1 is Point of (TOP-REAL n) : q1 in B } and A10: u = lower_bound G by A1, A7; A11: f . (p,q) in G by A8, A9; G c= f .: [:A,B:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] ) assume u in G ; ::_thesis: u in f .: [:A,B:] then consider q1 being Point of (TOP-REAL n) such that A12: u = f . (p,q1) and A13: q1 in B by A9; [p,q1] in [:A,B:] by A6, A13, ZFMISC_1:87; hence u in f .: [:A,B:] by A12, FUNCT_2:35; ::_thesis: verum end; hence u in f .: [:A,B:] by A3, A10, A11, Th2; ::_thesis: verum end; then A14: g .: A is bounded_below by A4, XXREAL_2:44; A15: for r being real number st r in f .: [:A,B:] holds lower_bound (g .: A) <= r proof let r be real number ; ::_thesis: ( r in f .: [:A,B:] implies lower_bound (g .: A) <= r ) assume r in f .: [:A,B:] ; ::_thesis: lower_bound (g .: A) <= r then consider pq being Point of [:(TOP-REAL n),(TOP-REAL n):] such that A16: pq in [:A,B:] and A17: r = f . pq by FUNCT_2:65; pq in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ; then pq in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2; then consider p, q being set such that A18: p in the carrier of (TOP-REAL n) and A19: q in the carrier of (TOP-REAL n) and A20: pq = [p,q] by ZFMISC_1:84; A21: q in B by A16, A20, ZFMISC_1:87; reconsider p = p, q = q as Point of (TOP-REAL n) by A18, A19; consider G being Subset of REAL such that A22: G = { (f . (p,q1)) where q1 is Point of (TOP-REAL n) : q1 in B } and A23: g . p = lower_bound G by A1; A24: p in A by A16, A20, ZFMISC_1:87; G c= f .: [:A,B:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] ) assume u in G ; ::_thesis: u in f .: [:A,B:] then consider q1 being Point of (TOP-REAL n) such that A25: u = f . (p,q1) and A26: q1 in B by A22; [p,q1] in [:A,B:] by A24, A26, ZFMISC_1:87; hence u in f .: [:A,B:] by A25, FUNCT_2:35; ::_thesis: verum end; then A27: G is bounded_below by A4, XXREAL_2:44; r = f . (p,q) by A17, A20; then r in G by A21, A22; then A28: g . p <= r by A23, A27, SEQ_4:def_2; g . p in g .: A by A24, FUNCT_2:35; then lower_bound (g .: A) <= g . p by A14, SEQ_4:def_2; hence lower_bound (g .: A) <= r by A28, XXREAL_0:2; ::_thesis: verum end; for s being real number st 0 < s holds ex r being real number st ( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s ) then consider r being real number such that A29: r in g .: A and A30: r < (lower_bound (g .: A)) + s by A14, SEQ_4:def_2; take r ; ::_thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s ) thus r in f .: [:A,B:] by A5, A29; ::_thesis: r < (lower_bound (g .: A)) + s thus r < (lower_bound (g .: A)) + s by A30; ::_thesis: verum end; hence lower_bound (f .: [:A,B:]) = lower_bound (g .: A) by A4, A15, SEQ_4:def_2; ::_thesis: verum end; theorem :: JORDAN_A:4 for n being Element of NAT for A, B being non empty compact Subset of (TOP-REAL n) for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: B) proof let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n) for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: B) let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):] for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: B) let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds lower_bound (f .: [:A,B:]) = lower_bound (g .: B) let g be RealMap of (TOP-REAL n); ::_thesis: ( ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: B) ) assume A1: for q being Point of (TOP-REAL n) ex G being Subset of REAL st ( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ; ::_thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: B) A2: [:A,B:] is compact by BORSUK_3:23; then A3: f .: [:A,B:] is compact by Th1; A4: f .: [:A,B:] is real-bounded by A2, Th1, RCOMP_1:10; A5: g .: B c= f .: [:A,B:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in g .: B or u in f .: [:A,B:] ) assume u in g .: B ; ::_thesis: u in f .: [:A,B:] then consider q being Point of (TOP-REAL n) such that A6: q in B and A7: u = g . q by FUNCT_2:65; consider p being Point of (TOP-REAL n) such that A8: p in A by SUBSET_1:4; consider G being Subset of REAL such that A9: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and A10: u = lower_bound G by A1, A7; A11: f . (p,q) in G by A8, A9; G c= f .: [:A,B:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] ) assume u in G ; ::_thesis: u in f .: [:A,B:] then consider p1 being Point of (TOP-REAL n) such that A12: u = f . (p1,q) and A13: p1 in A by A9; [p1,q] in [:A,B:] by A6, A13, ZFMISC_1:87; hence u in f .: [:A,B:] by A12, FUNCT_2:35; ::_thesis: verum end; hence u in f .: [:A,B:] by A3, A10, A11, Th2; ::_thesis: verum end; then A14: g .: B is bounded_below by A4, XXREAL_2:44; A15: for r being real number st r in f .: [:A,B:] holds lower_bound (g .: B) <= r proof let r be real number ; ::_thesis: ( r in f .: [:A,B:] implies lower_bound (g .: B) <= r ) assume r in f .: [:A,B:] ; ::_thesis: lower_bound (g .: B) <= r then consider pq being Point of [:(TOP-REAL n),(TOP-REAL n):] such that A16: pq in [:A,B:] and A17: r = f . pq by FUNCT_2:65; pq in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ; then pq in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2; then consider p, q being set such that A18: p in the carrier of (TOP-REAL n) and A19: q in the carrier of (TOP-REAL n) and A20: pq = [p,q] by ZFMISC_1:84; A21: p in A by A16, A20, ZFMISC_1:87; reconsider p = p, q = q as Point of (TOP-REAL n) by A18, A19; consider G being Subset of REAL such that A22: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and A23: g . q = lower_bound G by A1; A24: q in B by A16, A20, ZFMISC_1:87; G c= f .: [:A,B:] proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] ) assume u in G ; ::_thesis: u in f .: [:A,B:] then consider p1 being Point of (TOP-REAL n) such that A25: u = f . (p1,q) and A26: p1 in A by A22; [p1,q] in [:A,B:] by A24, A26, ZFMISC_1:87; hence u in f .: [:A,B:] by A25, FUNCT_2:35; ::_thesis: verum end; then A27: G is bounded_below by A4, XXREAL_2:44; r = f . (p,q) by A17, A20; then r in G by A21, A22; then A28: g . q <= r by A23, A27, SEQ_4:def_2; g . q in g .: B by A24, FUNCT_2:35; then lower_bound (g .: B) <= g . q by A14, SEQ_4:def_2; hence lower_bound (g .: B) <= r by A28, XXREAL_0:2; ::_thesis: verum end; for s being real number st 0 < s holds ex r being real number st ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) then consider r being real number such that A29: r in g .: B and A30: r < (lower_bound (g .: B)) + s by A14, SEQ_4:def_2; take r ; ::_thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) thus r in f .: [:A,B:] by A5, A29; ::_thesis: r < (lower_bound (g .: B)) + s thus r < (lower_bound (g .: B)) + s by A30; ::_thesis: verum end; hence lower_bound (f .: [:A,B:]) = lower_bound (g .: B) by A4, A15, SEQ_4:def_2; ::_thesis: verum end; theorem Th5: :: JORDAN_A:5 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds LE E-max C,q,C proof let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds LE E-max C,q,C let q be Point of (TOP-REAL 2); ::_thesis: ( q in Lower_Arc C & q <> W-min C implies LE E-max C,q,C ) E-max C in Upper_Arc C by JORDAN7:1; hence ( q in Lower_Arc C & q <> W-min C implies LE E-max C,q,C ) by JORDAN6:def_10; ::_thesis: verum end; theorem Th6: :: JORDAN_A:6 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds LE q, E-max C,C proof let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds LE q, E-max C,C let q be Point of (TOP-REAL 2); ::_thesis: ( q in Upper_Arc C implies LE q, E-max C,C ) A1: E-max C in Lower_Arc C by JORDAN7:1; E-max C <> W-min C by TOPREAL5:19; hence ( q in Upper_Arc C implies LE q, E-max C,C ) by A1, JORDAN6:def_10; ::_thesis: verum end; begin definition let n be Element of NAT ; A1: [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:def_2; func Eucl_dist n -> RealMap of [:(TOP-REAL n),(TOP-REAL n):] means :Def1: :: JORDAN_A:def 1 for p, q being Point of (TOP-REAL n) holds it . (p,q) = |.(p - q).|; existence ex b1 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st for p, q being Point of (TOP-REAL n) holds b1 . (p,q) = |.(p - q).| proof deffunc H1( Point of (TOP-REAL n), Point of (TOP-REAL n)) -> Element of REAL = |.($1 - $2).|; A2: for p, q being Point of (TOP-REAL n) holds H1(p,q) in REAL ; consider f being Function of [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):],REAL such that A3: for p, q being Point of (TOP-REAL n) holds f . (p,q) = H1(p,q) from FUNCT_7:sch_1(A2); reconsider f = f as RealMap of [:(TOP-REAL n),(TOP-REAL n):] by A1; take f ; ::_thesis: for p, q being Point of (TOP-REAL n) holds f . (p,q) = |.(p - q).| let p, q be Point of (TOP-REAL n); ::_thesis: f . (p,q) = |.(p - q).| thus f . (p,q) = |.(p - q).| by A3; ::_thesis: verum end; uniqueness for b1, b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st ( for p, q being Point of (TOP-REAL n) holds b1 . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds b2 . (p,q) = |.(p - q).| ) holds b1 = b2 proof let IT1, IT2 be RealMap of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: ( ( for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds IT2 . (p,q) = |.(p - q).| ) implies IT1 = IT2 ) assume that A4: for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = |.(p - q).| and A5: for p, q being Point of (TOP-REAL n) holds IT2 . (p,q) = |.(p - q).| ; ::_thesis: IT1 = IT2 now__::_thesis:_for_p,_q_being_Point_of_(TOP-REAL_n)_holds_IT1_._(p,q)_=_IT2_._(p,q) let p, q be Point of (TOP-REAL n); ::_thesis: IT1 . (p,q) = IT2 . (p,q) thus IT1 . (p,q) = |.(p - q).| by A4 .= IT2 . (p,q) by A5 ; ::_thesis: verum end; hence IT1 = IT2 by A1, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines Eucl_dist JORDAN_A:def_1_:_ for n being Element of NAT for b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] holds ( b2 = Eucl_dist n iff for p, q being Point of (TOP-REAL n) holds b2 . (p,q) = |.(p - q).| ); definition let T be non empty TopSpace; let f be RealMap of T; redefine attr f is continuous means :: JORDAN_A:def 2 for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N; compatibility ( f is continuous iff for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) proof thus ( f is continuous implies for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) ::_thesis: ( ( for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) implies f is continuous ) proof assume A1: f is continuous ; ::_thesis: for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N let p be Point of T; ::_thesis: for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N let N be Neighbourhood of f . p; ::_thesis: ex V being a_neighborhood of p st f .: V c= N A2: f " (N `) = (f " N) ` by FUNCT_2:100; N ` is closed by RCOMP_1:def_5; then f " (N `) is closed by A1, PSCOMP_1:def_3; then A3: f " N is open by A2, TOPS_1:4; f . p in N by RCOMP_1:16; then p in f " N by FUNCT_2:38; then reconsider V = f " N as a_neighborhood of p by A3, CONNSP_2:3; take V ; ::_thesis: f .: V c= N thus f .: V c= N by FUNCT_1:75; ::_thesis: verum end; assume A4: for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ; ::_thesis: f is continuous let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not Y is closed or f " Y is closed ) assume Y is closed ; ::_thesis: f " Y is closed then (Y `) ` is closed ; then A5: Y ` is open by RCOMP_1:def_5; for p being Point of T st p in (f " Y) ` holds ex A being Subset of T st ( A is a_neighborhood of p & A c= (f " Y) ` ) proof let p be Point of T; ::_thesis: ( p in (f " Y) ` implies ex A being Subset of T st ( A is a_neighborhood of p & A c= (f " Y) ` ) ) assume p in (f " Y) ` ; ::_thesis: ex A being Subset of T st ( A is a_neighborhood of p & A c= (f " Y) ` ) then p in f " (Y `) by FUNCT_2:100; then f . p in Y ` by FUNCT_2:38; then consider N being Neighbourhood of f . p such that A6: N c= Y ` by A5, RCOMP_1:18; consider V being a_neighborhood of p such that A7: f .: V c= N by A4; take V ; ::_thesis: ( V is a_neighborhood of p & V c= (f " Y) ` ) thus V is a_neighborhood of p ; ::_thesis: V c= (f " Y) ` f .: V c= Y ` by A6, A7, XBOOLE_1:1; then A8: f " (f .: V) c= f " (Y `) by RELAT_1:143; V c= f " (f .: V) by FUNCT_2:42; then V c= f " (Y `) by A8, XBOOLE_1:1; hence V c= (f " Y) ` by FUNCT_2:100; ::_thesis: verum end; then (f " Y) ` is open by CONNSP_2:7; then ((f " Y) `) ` is closed by TOPS_1:4; hence f " Y is closed ; ::_thesis: verum end; end; :: deftheorem defines continuous JORDAN_A:def_2_:_ for T being non empty TopSpace for f being RealMap of T holds ( f is continuous iff for p being Point of T for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ); Lm1: for X, Y being TopSpace holds TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] proof let X, Y be TopSpace; ::_thesis: TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] set T = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):]; A1: the carrier of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] = [: the carrier of TopStruct(# the carrier of X, the topology of X #), the carrier of TopStruct(# the carrier of Y, the topology of Y #):] by BORSUK_1:def_2 .= the carrier of [:X,Y:] by BORSUK_1:def_2 ; set tau1 = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of TopStruct(# the carrier of X, the topology of X #), Y1 is Subset of TopStruct(# the carrier of Y, the topology of Y #) : ( X1 in the topology of TopStruct(# the carrier of X, the topology of X #) & Y1 in the topology of TopStruct(# the carrier of Y, the topology of Y #) ) } } ; set tau2 = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ; the topology of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of TopStruct(# the carrier of X, the topology of X #), Y1 is Subset of TopStruct(# the carrier of Y, the topology of Y #) : ( X1 in the topology of TopStruct(# the carrier of X, the topology of X #) & Y1 in the topology of TopStruct(# the carrier of Y, the topology of Y #) ) } } by BORSUK_1:def_2 .= { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } .= the topology of [:X,Y:] by A1, BORSUK_1:def_2 ; hence TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] by A1; ::_thesis: verum end; registration let n be Element of NAT ; cluster Eucl_dist n -> continuous ; coherence Eucl_dist n is continuous proof set f = Eucl_dist n; let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: according to JORDAN_A:def_2 ::_thesis: for N being Neighbourhood of (Eucl_dist n) . p ex V being a_neighborhood of p st (Eucl_dist n) .: V c= N let N be Neighbourhood of (Eucl_dist n) . p; ::_thesis: ex V being a_neighborhood of p st (Eucl_dist n) .: V c= N consider r being real number such that A1: 0 < r and A2: N = ].(((Eucl_dist n) . p) - r),(((Eucl_dist n) . p) + r).[ by RCOMP_1:def_6; p in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ; then p in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2; then consider p1, p2 being set such that A3: p1 in the carrier of (TOP-REAL n) and A4: p2 in the carrier of (TOP-REAL n) and A5: p = [p1,p2] by ZFMISC_1:84; reconsider p1 = p1, p2 = p2 as Point of (TOP-REAL n) by A3, A4; reconsider p19 = p1, p29 = p2 as Element of (Euclid n) by TOPREAL3:8; A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider q1 = p1, q2 = p2 as Point of (TopSpaceMetr (Euclid n)) ; reconsider U = Ball (p19,(r / 2)) as a_neighborhood of q1 by A1, GOBOARD6:91, XREAL_1:215; reconsider W = Ball (p29,(r / 2)) as a_neighborhood of q2 by A1, GOBOARD6:91, XREAL_1:215; reconsider V = [:U,W:] as a_neighborhood of p by A5, A6, Lm1; take V ; ::_thesis: (Eucl_dist n) .: V c= N let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (Eucl_dist n) .: V or s in N ) assume A7: s in (Eucl_dist n) .: V ; ::_thesis: s in N then reconsider s = s as Real ; consider q being Point of [:(TOP-REAL n),(TOP-REAL n):] such that A8: q in V and A9: (Eucl_dist n) . q = s by A7, FUNCT_2:65; q in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ; then q in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2; then consider q1, q2 being set such that A10: q1 in the carrier of (TOP-REAL n) and A11: q2 in the carrier of (TOP-REAL n) and A12: q = [q1,q2] by ZFMISC_1:84; reconsider q1 = q1, q2 = q2 as Point of (TOP-REAL n) by A10, A11; reconsider q19 = q1, q29 = q2 as Element of (Euclid n) by TOPREAL3:8; reconsider q199 = q19, q299 = q29, p199 = p19, p299 = p29 as Element of REAL n ; A13: q19 in Ball (p19,(r / 2)) by A8, A12, ZFMISC_1:87; A14: q29 in Ball (p29,(r / 2)) by A8, A12, ZFMISC_1:87; A15: dist (q19,p19) < r / 2 by A13, METRIC_1:11; A16: dist (q29,p29) < r / 2 by A14, METRIC_1:11; A17: |.(q1 - p1).| < r / 2 by A15, SPPOL_1:5; |.(q2 - p2).| < r / 2 by A16, SPPOL_1:5; then A18: |.(q1 - p1).| + |.(q2 - p2).| < (r / 2) + (r / 2) by A17, XREAL_1:8; A19: for p, q being Point of (TOP-REAL n) holds (Eucl_dist n) . [p,q] = |.(p - q).| proof let p, q be Point of (TOP-REAL n); ::_thesis: (Eucl_dist n) . [p,q] = |.(p - q).| thus (Eucl_dist n) . [p,q] = (Eucl_dist n) . (p,q) .= |.(p - q).| by Def1 ; ::_thesis: verum end; then A20: (Eucl_dist n) . p = |.(p1 - p2).| by A5; A21: s = |.(q1 - q2).| by A9, A12, A19; A22: (q1 - q2) - (p1 - p2) = ((q1 - q2) - p1) + p2 by EUCLID:47 .= (q1 - (q2 + p1)) + p2 by EUCLID:46 .= ((q1 - p1) - q2) + p2 by EUCLID:46 .= (q1 - p1) - (q2 - p2) by EUCLID:47 ; A23: |.((q1 - p1) - (q2 - p2)).| <= |.(q1 - p1).| + |.(q2 - p2).| by TOPRNS_1:30; A24: s - ((Eucl_dist n) . p) <= |.((q1 - q2) - (p1 - p2)).| by A20, A21, TOPRNS_1:32; ((Eucl_dist n) . p) - s <= |.((p1 - p2) - (q1 - q2)).| by A20, A21, TOPRNS_1:32; then ((Eucl_dist n) . p) - s <= |.((q1 - q2) - (p1 - p2)).| by TOPRNS_1:27; then ((Eucl_dist n) . p) - s <= |.(q1 - p1).| + |.(q2 - p2).| by A22, A23, XXREAL_0:2; then ((Eucl_dist n) . p) - s < r by A18, XXREAL_0:2; then A25: ((Eucl_dist n) . p) - r < s by XREAL_1:11; s - ((Eucl_dist n) . p) <= |.(q1 - p1).| + |.(q2 - p2).| by A22, A23, A24, XXREAL_0:2; then s - ((Eucl_dist n) . p) < r by A18, XXREAL_0:2; then s < ((Eucl_dist n) . p) + r by XREAL_1:19; hence s in N by A2, A25, XXREAL_1:4; ::_thesis: verum end; end; begin theorem Th7: :: JORDAN_A:7 for n being Element of NAT for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds dist_min (A,B) > 0 proof let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds dist_min (A,B) > 0 let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: ( A misses B implies dist_min (A,B) > 0 ) assume A1: A misses B ; ::_thesis: dist_min (A,B) > 0 A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that A3: A = A9 and A4: B = B9 and A5: dist_min (A,B) = min_dist_min (A9,B9) by JORDAN1K:def_1; A6: A9 is compact by A2, A3, COMPTS_1:23; B9 is compact by A2, A4, COMPTS_1:23; hence dist_min (A,B) > 0 by A1, A3, A4, A5, A6, JGRAPH_1:38; ::_thesis: verum end; begin theorem Th8: :: JORDAN_A:8 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) proof let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) let p, q be Point of (TOP-REAL 2); ::_thesis: ( LE p,q,C & LE q, E-max C,C & p <> q implies Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) ) assume that A1: LE p,q,C and A2: LE q, E-max C,C and A3: p <> q ; ::_thesis: Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50; A5: LE p, E-max C,C by A1, A2, JORDAN6:58; A6: p in Upper_Arc C by A1, A2, JORDAN17:3, JORDAN6:58; A7: q in Upper_Arc C by A2, JORDAN17:3; A8: Upper_Arc C c= C by JORDAN6:61; A9: now__::_thesis:_not_q_=_W-min_C assume q = W-min C ; ::_thesis: contradiction then LE q,p,C by A6, A8, JORDAN7:3; hence contradiction by A1, A3, JORDAN6:57; ::_thesis: verum end; defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C ); defpred S2[ Point of (TOP-REAL 2)] means ( LE p,$1, Upper_Arc C, W-min C, E-max C & LE $1,q, Upper_Arc C, W-min C, E-max C ); A10: for p1 being Point of (TOP-REAL 2) holds ( S1[p1] iff S2[p1] ) proof let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] ) hereby ::_thesis: ( S2[p1] implies S1[p1] ) assume that A11: LE p,p1,C and A12: LE p1,q,C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C & LE p1,q, Upper_Arc C, W-min C, E-max C ) hereby ::_thesis: LE p1,q, Upper_Arc C, W-min C, E-max C percases ( p1 = E-max C or p1 = W-min C or ( p1 <> E-max C & p1 <> W-min C ) ) ; suppose p1 = E-max C ; ::_thesis: LE p,p1, Upper_Arc C, W-min C, E-max C hence LE p,p1, Upper_Arc C, W-min C, E-max C by A4, A6, JORDAN5C:10; ::_thesis: verum end; suppose p1 = W-min C ; ::_thesis: LE p,p1, Upper_Arc C, W-min C, E-max C then LE p1,p,C by A6, A8, JORDAN7:3; then p = p1 by A11, JORDAN6:57; hence LE p,p1, Upper_Arc C, W-min C, E-max C by A5, JORDAN17:3, JORDAN5C:9; ::_thesis: verum end; supposethat A13: p1 <> E-max C and A14: p1 <> W-min C ; ::_thesis: LE p,p1, Upper_Arc C, W-min C, E-max C now__::_thesis:_not_p1_in_Lower_Arc_C assume A15: p1 in Lower_Arc C ; ::_thesis: contradiction p1 in Upper_Arc C by A2, A12, JORDAN17:3, JORDAN6:58; then p1 in (Upper_Arc C) /\ (Lower_Arc C) by A15, XBOOLE_0:def_4; then p1 in {(W-min C),(E-max C)} by JORDAN6:50; hence contradiction by A13, A14, TARSKI:def_2; ::_thesis: verum end; hence LE p,p1, Upper_Arc C, W-min C, E-max C by A11, JORDAN6:def_10; ::_thesis: verum end; end; end; percases ( q = E-max C or q <> E-max C ) ; supposeA16: q = E-max C ; ::_thesis: LE p1,q, Upper_Arc C, W-min C, E-max C then p1 in Upper_Arc C by A12, JORDAN17:3; hence LE p1,q, Upper_Arc C, W-min C, E-max C by A4, A16, JORDAN5C:10; ::_thesis: verum end; supposeA17: q <> E-max C ; ::_thesis: LE p1,q, Upper_Arc C, W-min C, E-max C now__::_thesis:_not_q_in_Lower_Arc_C assume q in Lower_Arc C ; ::_thesis: contradiction then q in (Upper_Arc C) /\ (Lower_Arc C) by A7, XBOOLE_0:def_4; then q in {(W-min C),(E-max C)} by JORDAN6:50; hence contradiction by A9, A17, TARSKI:def_2; ::_thesis: verum end; hence LE p1,q, Upper_Arc C, W-min C, E-max C by A12, JORDAN6:def_10; ::_thesis: verum end; end; end; assume that A18: LE p,p1, Upper_Arc C, W-min C, E-max C and A19: LE p1,q, Upper_Arc C, W-min C, E-max C ; ::_thesis: S1[p1] A20: p1 in Upper_Arc C by A18, JORDAN5C:def_3; hence LE p,p1,C by A6, A18, JORDAN6:def_10; ::_thesis: LE p1,q,C thus LE p1,q,C by A7, A19, A20, JORDAN6:def_10; ::_thesis: verum end; deffunc H1( set ) -> set = $1; set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ; set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ; A21: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A10); Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A9, JORDAN7:def_1; hence Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) by A21, JORDAN6:26; ::_thesis: verum end; theorem Th9: :: JORDAN_A:9 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) proof let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) let q be Point of (TOP-REAL 2); ::_thesis: ( LE E-max C,q,C implies Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) ) set p = E-max C; assume A1: LE E-max C,q,C ; ::_thesis: Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; A3: E-max C in Lower_Arc C by JORDAN7:1; A4: q in Lower_Arc C by A1, JORDAN17:4; A5: Lower_Arc C c= C by JORDAN6:61; A6: now__::_thesis:_not_q_=_W-min_C assume A7: q = W-min C ; ::_thesis: contradiction then E-max C = q by A1, JORDAN7:2; hence contradiction by A7, TOPREAL5:19; ::_thesis: verum end; defpred S1[ Point of (TOP-REAL 2)] means ( LE E-max C,$1,C & LE $1,q,C ); defpred S2[ Point of (TOP-REAL 2)] means ( LE E-max C,$1, Lower_Arc C, E-max C, W-min C & LE $1,q, Lower_Arc C, E-max C, W-min C ); A8: for p1 being Point of (TOP-REAL 2) holds ( S1[p1] iff S2[p1] ) proof let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] ) hereby ::_thesis: ( S2[p1] implies S1[p1] ) assume that A9: LE E-max C,p1,C and A10: LE p1,q,C ; ::_thesis: ( LE E-max C,p1, Lower_Arc C, E-max C, W-min C & LE p1,q, Lower_Arc C, E-max C, W-min C ) A11: p1 in Lower_Arc C by A9, JORDAN17:4; hence LE E-max C,p1, Lower_Arc C, E-max C, W-min C by A2, JORDAN5C:10; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C percases ( p1 = E-max C or p1 <> E-max C ) ; supposeA12: p1 = E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C then q in Lower_Arc C by A10, JORDAN17:4; hence LE p1,q, Lower_Arc C, E-max C, W-min C by A2, A12, JORDAN5C:10; ::_thesis: verum end; supposeA13: p1 <> E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C A14: now__::_thesis:_not_p1_=_W-min_C assume A15: p1 = W-min C ; ::_thesis: contradiction then LE p1, E-max C,C by A3, A5, JORDAN7:3; hence contradiction by A9, A15, JORDAN6:57, TOPREAL5:19; ::_thesis: verum end; now__::_thesis:_not_p1_in_Upper_Arc_C assume p1 in Upper_Arc C ; ::_thesis: contradiction then p1 in (Upper_Arc C) /\ (Lower_Arc C) by A11, XBOOLE_0:def_4; then p1 in {(W-min C),(E-max C)} by JORDAN6:50; hence contradiction by A13, A14, TARSKI:def_2; ::_thesis: verum end; hence LE p1,q, Lower_Arc C, E-max C, W-min C by A10, JORDAN6:def_10; ::_thesis: verum end; end; end; assume that A16: LE E-max C,p1, Lower_Arc C, E-max C, W-min C and A17: LE p1,q, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1] A18: p1 in Lower_Arc C by A16, JORDAN5C:def_3; p1 <> W-min C by A2, A6, A17, JORDAN6:55; hence LE E-max C,p1,C by A3, A16, A18, JORDAN6:def_10; ::_thesis: LE p1,q,C thus LE p1,q,C by A4, A6, A17, A18, JORDAN6:def_10; ::_thesis: verum end; deffunc H1( set ) -> set = $1; set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ; set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ; A19: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A8); Segment ((E-max C),q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A6, JORDAN7:def_1; hence Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by A19, JORDAN6:26; ::_thesis: verum end; theorem Th10: :: JORDAN_A:10 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) proof let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) let q be Point of (TOP-REAL 2); ::_thesis: ( LE E-max C,q,C implies Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) ) set p = W-min C; assume A1: LE E-max C,q,C ; ::_thesis: Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; A3: W-min C in Lower_Arc C by JORDAN7:1; A4: q in Lower_Arc C by A1, JORDAN17:4; A5: Lower_Arc C c= C by JORDAN6:61; defpred S1[ Point of (TOP-REAL 2)] means ( LE q,$1,C or ( q in C & $1 = W-min C ) ); defpred S2[ Point of (TOP-REAL 2)] means ( LE q,$1, Lower_Arc C, E-max C, W-min C & LE $1, W-min C, Lower_Arc C, E-max C, W-min C ); A6: for p1 being Point of (TOP-REAL 2) holds ( S1[p1] iff S2[p1] ) proof let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] ) hereby ::_thesis: ( S2[p1] implies S1[p1] ) assume A7: ( LE q,p1,C or ( q in C & p1 = W-min C ) ) ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) percases ( ( q = E-max C & LE q,p1,C ) or ( q <> E-max C & LE q,p1,C ) or ( q in C & p1 = W-min C ) ) by A7; supposethat A8: q = E-max C and A9: LE q,p1,C ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) A10: p1 in Lower_Arc C by A8, A9, JORDAN17:4; hence LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A8, JORDAN5C:10; ::_thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A10, JORDAN5C:10; ::_thesis: verum end; supposethat A11: q <> E-max C and A12: LE q,p1,C ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) A13: p1 in Lower_Arc C by A1, A12, JORDAN17:4, JORDAN6:58; A14: now__::_thesis:_not_q_=_W-min_C assume A15: q = W-min C ; ::_thesis: contradiction then LE q, E-max C,C by JORDAN7:3, SPRECT_1:14; hence contradiction by A1, A15, JORDAN6:57, TOPREAL5:19; ::_thesis: verum end; now__::_thesis:_not_q_in_Upper_Arc_C assume q in Upper_Arc C ; ::_thesis: contradiction then q in (Upper_Arc C) /\ (Lower_Arc C) by A4, XBOOLE_0:def_4; then q in {(E-max C),(W-min C)} by JORDAN6:def_9; hence contradiction by A11, A14, TARSKI:def_2; ::_thesis: verum end; hence LE q,p1, Lower_Arc C, E-max C, W-min C by A12, JORDAN6:def_10; ::_thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A13, JORDAN5C:10; ::_thesis: verum end; supposethat q in C and A16: p1 = W-min C ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) thus LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A4, A16, JORDAN5C:10; ::_thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A3, A16, JORDAN5C:9; ::_thesis: verum end; end; end; assume that A17: LE q,p1, Lower_Arc C, E-max C, W-min C and LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1] A18: p1 in Lower_Arc C by A17, JORDAN5C:def_3; A19: q in Lower_Arc C by A17, JORDAN5C:def_3; percases ( p1 <> W-min C or p1 = W-min C ) ; suppose p1 <> W-min C ; ::_thesis: S1[p1] hence S1[p1] by A17, A18, A19, JORDAN6:def_10; ::_thesis: verum end; suppose p1 = W-min C ; ::_thesis: S1[p1] hence S1[p1] by A4, A5; ::_thesis: verum end; end; end; deffunc H1( set ) -> set = $1; set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ; set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ; A20: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A6); Segment (q,(W-min C),C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by JORDAN7:def_1; hence Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) by A20, JORDAN6:26; ::_thesis: verum end; theorem Th11: :: JORDAN_A:11 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) proof let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) let p, q be Point of (TOP-REAL 2); ::_thesis: ( LE p,q,C & LE E-max C,p,C implies Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) ) assume that A1: LE p,q,C and A2: LE E-max C,p,C ; ::_thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) percases ( p = E-max C or p <> E-max C ) ; suppose p = E-max C ; ::_thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) hence Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A1, Th9; ::_thesis: verum end; supposeA3: p <> E-max C ; ::_thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) A4: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; A5: q in Lower_Arc C by A1, A2, JORDAN17:4, JORDAN6:58; A6: p in Lower_Arc C by A2, JORDAN17:4; A7: Lower_Arc C c= C by JORDAN6:61; A8: now__::_thesis:_not_p_=_W-min_C assume A9: p = W-min C ; ::_thesis: contradiction then LE p, E-max C,C by JORDAN17:2; hence contradiction by A2, A9, JORDAN6:57, TOPREAL5:19; ::_thesis: verum end; A10: now__::_thesis:_not_q_=_W-min_C assume A11: q = W-min C ; ::_thesis: contradiction then LE q,p,C by A6, A7, JORDAN7:3; hence contradiction by A1, A8, A11, JORDAN6:57; ::_thesis: verum end; defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C ); defpred S2[ Point of (TOP-REAL 2)] means ( LE p,$1, Lower_Arc C, E-max C, W-min C & LE $1,q, Lower_Arc C, E-max C, W-min C ); A12: for p1 being Point of (TOP-REAL 2) holds ( S1[p1] iff S2[p1] ) proof let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] ) hereby ::_thesis: ( S2[p1] implies S1[p1] ) assume that A13: LE p,p1,C and A14: LE p1,q,C ; ::_thesis: ( LE p,p1, Lower_Arc C, E-max C, W-min C & LE p1,q, Lower_Arc C, E-max C, W-min C ) A15: now__::_thesis:_not_p1_=_W-min_C assume A16: p1 = W-min C ; ::_thesis: contradiction then LE p1,p,C by A6, A7, JORDAN7:3; hence contradiction by A8, A13, A16, JORDAN6:57; ::_thesis: verum end; A17: now__::_thesis:_not_p_in_Upper_Arc_C assume A18: p in Upper_Arc C ; ::_thesis: contradiction p in Lower_Arc C by A2, JORDAN17:4; then p in (Lower_Arc C) /\ (Upper_Arc C) by A18, XBOOLE_0:def_4; then p in {(W-min C),(E-max C)} by JORDAN6:50; hence contradiction by A3, A8, TARSKI:def_2; ::_thesis: verum end; hence LE p,p1, Lower_Arc C, E-max C, W-min C by A13, JORDAN6:def_10; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C A19: p1 in Lower_Arc C by A13, A17, JORDAN6:def_10; percases ( q = E-max C or p1 = E-max C or p1 <> E-max C ) ; suppose q = E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C hence LE p1,q, Lower_Arc C, E-max C, W-min C by A1, A2, A3, JORDAN6:57; ::_thesis: verum end; suppose p1 = E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C hence LE p1,q, Lower_Arc C, E-max C, W-min C by A4, A5, JORDAN5C:10; ::_thesis: verum end; supposeA20: p1 <> E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C now__::_thesis:_not_p1_in_Upper_Arc_C assume p1 in Upper_Arc C ; ::_thesis: contradiction then p1 in (Lower_Arc C) /\ (Upper_Arc C) by A19, XBOOLE_0:def_4; then p1 in {(W-min C),(E-max C)} by JORDAN6:50; hence contradiction by A15, A20, TARSKI:def_2; ::_thesis: verum end; hence LE p1,q, Lower_Arc C, E-max C, W-min C by A14, JORDAN6:def_10; ::_thesis: verum end; end; end; assume that A21: LE p,p1, Lower_Arc C, E-max C, W-min C and A22: LE p1,q, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1] A23: p1 <> W-min C by A4, A10, A22, JORDAN6:55; A24: p1 in Lower_Arc C by A21, JORDAN5C:def_3; hence LE p,p1,C by A6, A21, A23, JORDAN6:def_10; ::_thesis: LE p1,q,C thus LE p1,q,C by A5, A10, A22, A24, JORDAN6:def_10; ::_thesis: verum end; deffunc H1( set ) -> set = $1; set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ; set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ; A25: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A12); Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A10, JORDAN7:def_1; hence Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A25, JORDAN6:26; ::_thesis: verum end; end; end; theorem Th12: :: JORDAN_A:12 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) proof let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) let p, q be Point of (TOP-REAL 2); ::_thesis: ( LE p, E-max C,C & LE E-max C,q,C implies Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) ) assume that A1: LE p, E-max C,C and A2: LE E-max C,q,C ; ::_thesis: Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) A3: p in Upper_Arc C by A1, JORDAN17:3; A4: q in Lower_Arc C by A2, JORDAN17:4; A5: now__::_thesis:_not_q_=_W-min_C assume q = W-min C ; ::_thesis: contradiction then W-min C = E-max C by A2, JORDAN7:2; hence contradiction by TOPREAL5:19; ::_thesis: verum end; A6: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C ); defpred S2[ Point of (TOP-REAL 2)] means LE p,$1, Upper_Arc C, W-min C, E-max C; defpred S3[ Point of (TOP-REAL 2)] means LE $1,q, Lower_Arc C, E-max C, W-min C; defpred S4[ Point of (TOP-REAL 2)] means ( S2[$1] or S3[$1] ); A7: for p1 being Point of (TOP-REAL 2) holds ( S1[p1] iff S4[p1] ) proof let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S4[p1] ) thus ( LE p,p1,C & LE p1,q,C & not LE p,p1, Upper_Arc C, W-min C, E-max C implies LE p1,q, Lower_Arc C, E-max C, W-min C ) ::_thesis: ( S4[p1] implies S1[p1] ) proof assume that A8: LE p,p1,C and A9: LE p1,q,C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) A10: now__::_thesis:_(_p1_in_Lower_Arc_C_&_p1_in_Upper_Arc_C_&_not_p1_=_W-min_C_implies_p1_=_E-max_C_) assume that A11: p1 in Lower_Arc C and A12: p1 in Upper_Arc C ; ::_thesis: ( p1 = W-min C or p1 = E-max C ) p1 in (Lower_Arc C) /\ (Upper_Arc C) by A11, A12, XBOOLE_0:def_4; then p1 in {(W-min C),(E-max C)} by JORDAN6:def_9; hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def_2; ::_thesis: verum end; percases ( p1 = W-min C or p1 = E-max C or not p1 in Lower_Arc C or not p1 in Upper_Arc C ) by A10; supposeA13: p1 = W-min C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) then p = W-min C by A8, JORDAN7:2; hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A1, A13, JORDAN17:3, JORDAN5C:9; ::_thesis: verum end; suppose p1 = E-max C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A4, A6, JORDAN5C:10; ::_thesis: verum end; suppose not p1 in Lower_Arc C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A8, JORDAN6:def_10; ::_thesis: verum end; suppose not p1 in Upper_Arc C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A9, JORDAN6:def_10; ::_thesis: verum end; end; end; assume A14: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) ; ::_thesis: S1[p1] percases ( LE p,p1, Upper_Arc C, W-min C, E-max C or ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 <> W-min C ) or ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 = W-min C ) ) by A14; supposeA15: LE p,p1, Upper_Arc C, W-min C, E-max C ; ::_thesis: S1[p1] then A16: p1 in Upper_Arc C by JORDAN5C:def_3; hence LE p,p1,C by A3, A15, JORDAN6:def_10; ::_thesis: LE p1,q,C thus LE p1,q,C by A4, A5, A16, JORDAN6:def_10; ::_thesis: verum end; supposethat A17: LE p1,q, Lower_Arc C, E-max C, W-min C and A18: p1 <> W-min C ; ::_thesis: S1[p1] A19: p1 in Lower_Arc C by A17, JORDAN5C:def_3; hence LE p,p1,C by A3, A18, JORDAN6:def_10; ::_thesis: LE p1,q,C thus LE p1,q,C by A4, A5, A17, A19, JORDAN6:def_10; ::_thesis: verum end; suppose ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 = W-min C ) ; ::_thesis: S1[p1] hence S1[p1] by A5, A6, JORDAN6:55; ::_thesis: verum end; end; end; set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } ; set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } ; deffunc H1( set ) -> set = $1; set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ; set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } ; set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } ; A20: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } from FRAENKEL:sch_3(A7); A21: Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A5, JORDAN7:def_1; A22: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } by JORDAN6:def_3; { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } from TOPREAL1:sch_1(); hence Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A20, A21, A22, JORDAN6:def_4; ::_thesis: verum end; theorem Th13: :: JORDAN_A:13 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) proof let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) let p be Point of (TOP-REAL 2); ::_thesis: ( LE p, E-max C,C implies Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) ) set q = W-min C; assume LE p, E-max C,C ; ::_thesis: Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) then A1: p in Upper_Arc C by JORDAN17:3; A2: W-min C in Lower_Arc C by JORDAN7:1; A3: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C or ( p in C & $1 = W-min C ) ); defpred S2[ Point of (TOP-REAL 2)] means LE p,$1, Upper_Arc C, W-min C, E-max C; defpred S3[ Point of (TOP-REAL 2)] means LE $1, W-min C, Lower_Arc C, E-max C, W-min C; defpred S4[ Point of (TOP-REAL 2)] means ( S2[$1] or S3[$1] ); A4: for p1 being Point of (TOP-REAL 2) holds ( S1[p1] iff S4[p1] ) proof let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S4[p1] ) thus ( ( not LE p,p1,C & not ( p in C & p1 = W-min C ) ) or LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) ::_thesis: ( S4[p1] implies S1[p1] ) proof assume A5: ( LE p,p1,C or ( p in C & p1 = W-min C ) ) ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) A6: now__::_thesis:_(_p1_in_Lower_Arc_C_&_p1_in_Upper_Arc_C_&_not_p1_=_W-min_C_implies_p1_=_E-max_C_) assume that A7: p1 in Lower_Arc C and A8: p1 in Upper_Arc C ; ::_thesis: ( p1 = W-min C or p1 = E-max C ) p1 in (Lower_Arc C) /\ (Upper_Arc C) by A7, A8, XBOOLE_0:def_4; then p1 in {(W-min C),(E-max C)} by JORDAN6:def_9; hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def_2; ::_thesis: verum end; percases ( p1 = W-min C or p1 = E-max C or ( not p1 in Lower_Arc C & p1 <> W-min C ) or ( not p1 in Upper_Arc C & p1 <> W-min C ) ) by A6; suppose p1 = W-min C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A2, JORDAN5C:9; ::_thesis: verum end; suppose p1 = E-max C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A2, A3, JORDAN5C:10; ::_thesis: verum end; suppose ( not p1 in Lower_Arc C & p1 <> W-min C ) ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A5, JORDAN6:def_10; ::_thesis: verum end; supposethat A9: not p1 in Upper_Arc C and A10: p1 <> W-min C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) A11: p1 in C by A5, A10, JORDAN7:5; C = (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:def_9; then p1 in Lower_Arc C by A9, A11, XBOOLE_0:def_3; hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A3, JORDAN5C:10; ::_thesis: verum end; end; end; assume A12: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) ; ::_thesis: S1[p1] A13: Upper_Arc C c= C by JORDAN6:61; percases ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A12; supposeA14: LE p,p1, Upper_Arc C, W-min C, E-max C ; ::_thesis: S1[p1] then p1 in Upper_Arc C by JORDAN5C:def_3; hence S1[p1] by A1, A14, JORDAN6:def_10; ::_thesis: verum end; suppose LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1] then A15: p1 in Lower_Arc C by JORDAN5C:def_3; now__::_thesis:_S1[p1] percases ( p1 = W-min C or p1 <> W-min C ) ; suppose p1 = W-min C ; ::_thesis: S1[p1] hence S1[p1] by A1, A13; ::_thesis: verum end; suppose p1 <> W-min C ; ::_thesis: S1[p1] hence S1[p1] by A1, A15, JORDAN6:def_10; ::_thesis: verum end; end; end; hence S1[p1] ; ::_thesis: verum end; end; end; set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } ; set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } ; deffunc H1( set ) -> set = $1; set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ; set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } ; set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } ; A16: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } from FRAENKEL:sch_3(A4); A17: Segment (p,(W-min C),C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by JORDAN7:def_1; A18: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } by JORDAN6:def_3; { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } from TOPREAL1:sch_1(); hence Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A16, A17, A18, JORDAN6:def_4; ::_thesis: verum end; theorem Th14: :: JORDAN_A:14 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) holds R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) proof let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) holds R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) let p be Point of (TOP-REAL 2); ::_thesis: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50; then L_Segment ((Upper_Arc C),(W-min C),(E-max C),(E-max C)) = Upper_Arc C by JORDAN6:22; hence Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (Upper_Arc C) by JORDAN6:def_5 .= R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by JORDAN6:20, XBOOLE_1:28 ; ::_thesis: verum end; theorem Th15: :: JORDAN_A:15 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) proof let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) let p be Point of (TOP-REAL 2); ::_thesis: L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; then R_Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C)) = Lower_Arc C by JORDAN6:24; hence Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) = (Lower_Arc C) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),p)) by JORDAN6:def_5 .= L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) by JORDAN6:19, XBOOLE_1:28 ; ::_thesis: verum end; theorem Th16: :: JORDAN_A:16 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds Segment (p,(W-min C),C) is_an_arc_of p, W-min C proof let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds Segment (p,(W-min C),C) is_an_arc_of p, W-min C set q = W-min C; let p be Point of (TOP-REAL 2); ::_thesis: ( p in C & p <> W-min C implies Segment (p,(W-min C),C) is_an_arc_of p, W-min C ) assume that A1: p in C and A2: p <> W-min C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C A3: E-max C in C by SPRECT_1:14; A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50; A5: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; A6: W-min C <> E-max C by TOPREAL5:19; percases ( ( p <> E-max C & LE p, E-max C,C ) or p = E-max C or ( p <> E-max C & LE E-max C,p,C ) ) by A1, A3, JORDAN16:7; supposethat A7: p <> E-max C and A8: LE p, E-max C,C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C A9: now__::_thesis:_not_W-min_C_in_(R_Segment_((Upper_Arc_C),(W-min_C),(E-max_C),p))_/\_(L_Segment_((Lower_Arc_C),(E-max_C),(W-min_C),(W-min_C))) assume W-min C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) ; ::_thesis: contradiction then W-min C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by XBOOLE_0:def_4; hence contradiction by A2, A4, JORDAN6:60; ::_thesis: verum end; p in Upper_Arc C by A8, JORDAN17:3; then A10: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A4, JORDAN5C:10; A11: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) by Th14; then A12: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A10, JORDAN16:5; W-min C in Lower_Arc C by JORDAN7:1; then A13: LE E-max C, W-min C, Lower_Arc C, E-max C, W-min C by A5, JORDAN5C:10; A14: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),(W-min C)) by Th15; then E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) by A13, JORDAN16:5; then A15: E-max C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A12, XBOOLE_0:def_4; A16: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) c= Upper_Arc C by JORDAN6:20; A17: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) c= Lower_Arc C by JORDAN6:19; (Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def_9; then A18: (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) = {(E-max C)} by A9, A15, A16, A17, TOPREAL8:1, XBOOLE_1:27; A19: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) is_an_arc_of p, E-max C by A4, A7, A10, A11, JORDAN16:21; A20: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) is_an_arc_of E-max C, W-min C by A5, A6, A13, A14, JORDAN16:21; Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A8, Th13; hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A18, A19, A20, TOPREAL1:2; ::_thesis: verum end; supposeA21: p = E-max C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C then Segment (p,(W-min C),C) = Lower_Arc C by JORDAN7:4; hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A21, JORDAN6:50; ::_thesis: verum end; supposethat p <> E-max C and A22: LE E-max C,p,C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C A23: Segment (p,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,(W-min C)) by A22, Th10; p in Lower_Arc C by A22, JORDAN17:4; then LE p, W-min C, Lower_Arc C, E-max C, W-min C by A5, JORDAN5C:10; hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A2, A5, A23, JORDAN16:21; ::_thesis: verum end; end; end; theorem Th17: :: JORDAN_A:17 for C being Simple_closed_curve for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds Segment (p,q,C) is_an_arc_of p,q proof let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds Segment (p,q,C) is_an_arc_of p,q let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & LE p,q,C implies Segment (p,q,C) is_an_arc_of p,q ) assume that A1: p <> q and A2: LE p,q,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q A3: E-max C in C by SPRECT_1:14; A4: p in C by A2, JORDAN7:5; A5: q in C by A2, JORDAN7:5; A6: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50; A7: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50; percases ( q = W-min C or ( LE q, E-max C,C & not LE E-max C,q,C & q <> W-min C ) or ( p <> E-max C & LE p, E-max C,C & LE E-max C,q,C & q <> E-max C ) or ( q = E-max C & LE p, E-max C,C & LE E-max C,q,C ) or ( p = E-max C & LE p, E-max C,C & LE E-max C,q,C ) or ( LE E-max C,p,C & not LE p, E-max C,C ) ) by A3, A4, A5, JORDAN16:7; suppose q = W-min C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q hence Segment (p,q,C) is_an_arc_of p,q by A1, A4, Th16; ::_thesis: verum end; supposethat A8: LE q, E-max C,C and A9: not LE E-max C,q,C and A10: q <> W-min C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q A11: Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) by A1, A2, A8, Th8; not q in Lower_Arc C by A9, A10, Th5; then LE p,q, Upper_Arc C, W-min C, E-max C by A2, JORDAN6:def_10; hence Segment (p,q,C) is_an_arc_of p,q by A1, A6, A11, JORDAN16:21; ::_thesis: verum end; supposethat A12: p <> E-max C and A13: LE p, E-max C,C and A14: LE E-max C,q,C and A15: q <> E-max C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q A16: now__::_thesis:_not_W-min_C_in_(R_Segment_((Upper_Arc_C),(W-min_C),(E-max_C),p))_/\_(L_Segment_((Lower_Arc_C),(E-max_C),(W-min_C),q)) assume A17: W-min C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) ; ::_thesis: contradiction then W-min C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by XBOOLE_0:def_4; then A18: p = W-min C by A6, JORDAN6:60; W-min C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A17, XBOOLE_0:def_4; hence contradiction by A1, A7, A18, JORDAN6:59; ::_thesis: verum end; p in Upper_Arc C by A13, JORDAN17:3; then A19: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A6, JORDAN5C:10; A20: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) by Th14; then A21: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A19, JORDAN16:5; q in Lower_Arc C by A14, JORDAN17:4; then A22: LE E-max C,q, Lower_Arc C, E-max C, W-min C by A7, JORDAN5C:10; A23: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by Th15; then E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A22, JORDAN16:5; then A24: E-max C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A21, XBOOLE_0:def_4; A25: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) c= Upper_Arc C by JORDAN6:20; A26: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) c= Lower_Arc C by JORDAN6:19; (Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def_9; then A27: (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) = {(E-max C)} by A16, A24, A25, A26, TOPREAL8:1, XBOOLE_1:27; A28: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) is_an_arc_of p, E-max C by A6, A12, A19, A20, JORDAN16:21; A29: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) is_an_arc_of E-max C,q by A7, A15, A22, A23, JORDAN16:21; Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A13, A14, Th12; hence Segment (p,q,C) is_an_arc_of p,q by A27, A28, A29, TOPREAL1:2; ::_thesis: verum end; supposethat A30: q = E-max C and A31: LE p, E-max C,C and A32: LE E-max C,q,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q p in Upper_Arc C by A31, JORDAN17:3; then A33: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A6, JORDAN5C:10; A34: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) by Th14; then A35: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A33, JORDAN16:5; A36: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = {(E-max C)} by A7, A30, JORDAN6:21; Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A31, A32, Th12 .= R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A35, A36, ZFMISC_1:40 ; hence Segment (p,q,C) is_an_arc_of p,q by A1, A6, A30, A33, A34, JORDAN16:21; ::_thesis: verum end; supposethat A37: p = E-max C and A38: LE p, E-max C,C and A39: LE E-max C,q,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q q in Lower_Arc C by A39, JORDAN17:4; then A40: LE E-max C,q, Lower_Arc C, E-max C, W-min C by A7, JORDAN5C:10; A41: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by Th15; then A42: E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A40, JORDAN16:5; A43: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = {(E-max C)} by A6, A37, JORDAN6:23; Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A38, A39, Th12 .= L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A42, A43, ZFMISC_1:40 ; hence Segment (p,q,C) is_an_arc_of p,q by A1, A7, A37, A40, A41, JORDAN16:21; ::_thesis: verum end; supposethat A44: LE E-max C,p,C and A45: not LE p, E-max C,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q A46: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A2, A44, Th11; not p in Upper_Arc C by A45, Th6; then LE p,q, Lower_Arc C, E-max C, W-min C by A2, JORDAN6:def_10; hence Segment (p,q,C) is_an_arc_of p,q by A1, A7, A46, JORDAN16:21; ::_thesis: verum end; end; end; theorem Th18: :: JORDAN_A:18 for C being Simple_closed_curve holds C = Segment ((W-min C),(W-min C),C) proof let C be Simple_closed_curve; ::_thesis: C = Segment ((W-min C),(W-min C),C) set X = { p where p is Point of (TOP-REAL 2) : ( LE W-min C,p,C or ( W-min C in C & p = W-min C ) ) } ; A1: Segment ((W-min C),(W-min C),C) = { p where p is Point of (TOP-REAL 2) : ( LE W-min C,p,C or ( W-min C in C & p = W-min C ) ) } by JORDAN7:def_1; thus C c= Segment ((W-min C),(W-min C),C) :: according to XBOOLE_0:def_10 ::_thesis: Segment ((W-min C),(W-min C),C) c= C proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in C or e in Segment ((W-min C),(W-min C),C) ) assume A2: e in C ; ::_thesis: e in Segment ((W-min C),(W-min C),C) then reconsider p = e as Point of (TOP-REAL 2) ; LE W-min C,p,C by A2, JORDAN7:3; hence e in Segment ((W-min C),(W-min C),C) by A1; ::_thesis: verum end; thus Segment ((W-min C),(W-min C),C) c= C by JORDAN16:6; ::_thesis: verum end; theorem Th19: :: JORDAN_A:19 for C being Simple_closed_curve for q being Point of (TOP-REAL 2) st q in C holds Segment (q,(W-min C),C) is compact proof let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st q in C holds Segment (q,(W-min C),C) is compact let q be Point of (TOP-REAL 2); ::_thesis: ( q in C implies Segment (q,(W-min C),C) is compact ) assume A1: q in C ; ::_thesis: Segment (q,(W-min C),C) is compact percases ( q = W-min C or q <> W-min C ) ; suppose q = W-min C ; ::_thesis: Segment (q,(W-min C),C) is compact hence Segment (q,(W-min C),C) is compact by Th18; ::_thesis: verum end; suppose q <> W-min C ; ::_thesis: Segment (q,(W-min C),C) is compact hence Segment (q,(W-min C),C) is compact by A1, Th16, JORDAN5A:1; ::_thesis: verum end; end; end; theorem Th20: :: JORDAN_A:20 for C being Simple_closed_curve for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds Segment (q1,q2,C) is compact proof let C be Simple_closed_curve; ::_thesis: for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds Segment (q1,q2,C) is compact let q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( LE q1,q2,C implies Segment (q1,q2,C) is compact ) assume A1: LE q1,q2,C ; ::_thesis: Segment (q1,q2,C) is compact A2: q1 in C by A1, JORDAN7:5; percases ( q2 = W-min C or ( q1 = q2 & q2 <> W-min C ) or ( q1 <> q2 & q2 <> W-min C ) ) ; suppose q2 = W-min C ; ::_thesis: Segment (q1,q2,C) is compact hence Segment (q1,q2,C) is compact by A2, Th19; ::_thesis: verum end; suppose ( q1 = q2 & q2 <> W-min C ) ; ::_thesis: Segment (q1,q2,C) is compact then Segment (q1,q2,C) = {q1} by A2, JORDAN7:8; hence Segment (q1,q2,C) is compact ; ::_thesis: verum end; suppose ( q1 <> q2 & q2 <> W-min C ) ; ::_thesis: Segment (q1,q2,C) is compact hence Segment (q1,q2,C) is compact by A1, Th17, JORDAN5A:1; ::_thesis: verum end; end; end; begin definition let C be Simple_closed_curve; mode Segmentation of C -> FinSequence of (TOP-REAL 2) means :Def3: :: JORDAN_A:def 3 ( it /. 1 = W-min C & it is one-to-one & 8 <= len it & rng it c= C & ( for i being Element of NAT st 1 <= i & i < len it holds LE it /. i,it /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len it holds (Segment ((it /. i),(it /. (i + 1)),C)) /\ (Segment ((it /. (i + 1)),(it /. (i + 2)),C)) = {(it /. (i + 1))} ) & (Segment ((it /. (len it)),(it /. 1),C)) /\ (Segment ((it /. 1),(it /. 2),C)) = {(it /. 1)} & (Segment ((it /. ((len it) -' 1)),(it /. (len it)),C)) /\ (Segment ((it /. (len it)),(it /. 1),C)) = {(it /. (len it))} & Segment ((it /. ((len it) -' 1)),(it /. (len it)),C) misses Segment ((it /. 1),(it /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len it & not i,j are_adjacent1 holds Segment ((it /. i),(it /. (i + 1)),C) misses Segment ((it /. j),(it /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len it holds Segment ((it /. (len it)),(it /. 1),C) misses Segment ((it /. i),(it /. (i + 1)),C) ) ); existence ex b1 being FinSequence of (TOP-REAL 2) st ( b1 /. 1 = W-min C & b1 is one-to-one & 8 <= len b1 & rng b1 c= C & ( for i being Element of NAT st 1 <= i & i < len b1 holds LE b1 /. i,b1 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b1 holds (Segment ((b1 /. i),(b1 /. (i + 1)),C)) /\ (Segment ((b1 /. (i + 1)),(b1 /. (i + 2)),C)) = {(b1 /. (i + 1))} ) & (Segment ((b1 /. (len b1)),(b1 /. 1),C)) /\ (Segment ((b1 /. 1),(b1 /. 2),C)) = {(b1 /. 1)} & (Segment ((b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C)) /\ (Segment ((b1 /. (len b1)),(b1 /. 1),C)) = {(b1 /. (len b1))} & Segment ((b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C) misses Segment ((b1 /. 1),(b1 /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b1 & not i,j are_adjacent1 holds Segment ((b1 /. i),(b1 /. (i + 1)),C) misses Segment ((b1 /. j),(b1 /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len b1 holds Segment ((b1 /. (len b1)),(b1 /. 1),C) misses Segment ((b1 /. i),(b1 /. (i + 1)),C) ) ) proof consider h being FinSequence of the carrier of (TOP-REAL 2) such that A1: h . 1 = W-min C and A2: h is one-to-one and A3: 8 <= len h and A4: rng h c= C and A5: for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C and for i being Element of NAT for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),C) holds diameter W < 1 and for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),C) holds diameter W < 1 and A6: for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} and A7: (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} and A8: (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} and A9: Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) and A10: for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and A11: for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by JORDAN7:20; reconsider h = h as non empty FinSequence of the carrier of (TOP-REAL 2) by A3, CARD_1:27; take h ; ::_thesis: ( h /. 1 = W-min C & h is one-to-one & 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) 1 in dom h by FINSEQ_5:6; hence h /. 1 = W-min C by A1, PARTFUN1:def_6; ::_thesis: ( h is one-to-one & 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus h is one-to-one by A2; ::_thesis: ( 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus 8 <= len h by A3; ::_thesis: ( rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus rng h c= C by A4; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C by A5; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} by A6; ::_thesis: ( (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} by A7; ::_thesis: ( (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} by A8; ::_thesis: ( Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) by A9; ::_thesis: ( ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) ) thus for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) by A10; ::_thesis: for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) thus for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by A11; ::_thesis: verum end; end; :: deftheorem Def3 defines Segmentation JORDAN_A:def_3_:_ for C being Simple_closed_curve for b2 being FinSequence of (TOP-REAL 2) holds ( b2 is Segmentation of C iff ( b2 /. 1 = W-min C & b2 is one-to-one & 8 <= len b2 & rng b2 c= C & ( for i being Element of NAT st 1 <= i & i < len b2 holds LE b2 /. i,b2 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b2 holds (Segment ((b2 /. i),(b2 /. (i + 1)),C)) /\ (Segment ((b2 /. (i + 1)),(b2 /. (i + 2)),C)) = {(b2 /. (i + 1))} ) & (Segment ((b2 /. (len b2)),(b2 /. 1),C)) /\ (Segment ((b2 /. 1),(b2 /. 2),C)) = {(b2 /. 1)} & (Segment ((b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C)) /\ (Segment ((b2 /. (len b2)),(b2 /. 1),C)) = {(b2 /. (len b2))} & Segment ((b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C) misses Segment ((b2 /. 1),(b2 /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b2 & not i,j are_adjacent1 holds Segment ((b2 /. i),(b2 /. (i + 1)),C) misses Segment ((b2 /. j),(b2 /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len b2 holds Segment ((b2 /. (len b2)),(b2 /. 1),C) misses Segment ((b2 /. i),(b2 /. (i + 1)),C) ) ) ); registration let C be Simple_closed_curve; cluster -> non trivial for Segmentation of C; coherence for b1 being Segmentation of C holds not b1 is trivial proof let S be Segmentation of C; ::_thesis: not S is trivial len S >= 8 by Def3; then len S >= 2 by XXREAL_0:2; hence not S is trivial by NAT_D:60; ::_thesis: verum end; end; theorem Th21: :: JORDAN_A:21 for C being Simple_closed_curve for S being Segmentation of C for i being Element of NAT st 1 <= i & i <= len S holds S /. i in C proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for i being Element of NAT st 1 <= i & i <= len S holds S /. i in C let S be Segmentation of C; ::_thesis: for i being Element of NAT st 1 <= i & i <= len S holds S /. i in C let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len S implies S /. i in C ) assume that A1: 1 <= i and A2: i <= len S ; ::_thesis: S /. i in C i in dom S by A1, A2, FINSEQ_3:25; then A3: S /. i in rng S by PARTFUN2:2; rng S c= C by Def3; hence S /. i in C by A3; ::_thesis: verum end; begin definition let C be Simple_closed_curve; let i be Nat; let S be Segmentation of C; func Segm (S,i) -> Subset of (TOP-REAL 2) equals :Def4: :: JORDAN_A:def 4 Segment ((S /. i),(S /. (i + 1)),C) if ( 1 <= i & i < len S ) otherwise Segment ((S /. (len S)),(S /. 1),C); correctness coherence ( ( 1 <= i & i < len S implies Segment ((S /. i),(S /. (i + 1)),C) is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len S ) implies Segment ((S /. (len S)),(S /. 1),C) is Subset of (TOP-REAL 2) ) ); consistency for b1 being Subset of (TOP-REAL 2) holds verum; ; end; :: deftheorem Def4 defines Segm JORDAN_A:def_4_:_ for C being Simple_closed_curve for i being Nat for S being Segmentation of C holds ( ( 1 <= i & i < len S implies Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) ) & ( ( not 1 <= i or not i < len S ) implies Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) ); theorem :: JORDAN_A:22 for C being Simple_closed_curve for i being Element of NAT for S being Segmentation of C st i in dom S holds Segm (S,i) c= C proof let C be Simple_closed_curve; ::_thesis: for i being Element of NAT for S being Segmentation of C st i in dom S holds Segm (S,i) c= C let i be Element of NAT ; ::_thesis: for S being Segmentation of C st i in dom S holds Segm (S,i) c= C let S be Segmentation of C; ::_thesis: ( i in dom S implies Segm (S,i) c= C ) assume i in dom S ; ::_thesis: Segm (S,i) c= C then A1: 1 <= i by FINSEQ_3:25; ( i < len S or i >= len S ) ; then ( Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) or Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) by A1, Def4; hence Segm (S,i) c= C by JORDAN16:6; ::_thesis: verum end; registration let C be Simple_closed_curve; let S be Segmentation of C; let i be Element of NAT ; cluster Segm (S,i) -> non empty compact ; coherence ( not Segm (S,i) is empty & Segm (S,i) is compact ) proof percases ( ( 1 <= i & i < len S ) or not 1 <= i or not i < len S ) ; supposeA1: ( 1 <= i & i < len S ) ; ::_thesis: ( not Segm (S,i) is empty & Segm (S,i) is compact ) then A2: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by Def4; LE S /. i,S /. (i + 1),C by A1, Def3; hence ( not Segm (S,i) is empty & Segm (S,i) is compact ) by A2, Th20, JORDAN7:6; ::_thesis: verum end; suppose ( not 1 <= i or not i < len S ) ; ::_thesis: ( not Segm (S,i) is empty & Segm (S,i) is compact ) then A3: Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) by Def4; 8 <= len S by Def3; then 1 <= len S by XXREAL_0:2; then A4: S /. (len S) in C by Th21; S /. 1 = W-min C by Def3; hence ( not Segm (S,i) is empty & Segm (S,i) is compact ) by A3, A4, Th19, JORDAN16:19; ::_thesis: verum end; end; end; end; theorem :: JORDAN_A:23 for C being Simple_closed_curve for S being Segmentation of C for p being Point of (TOP-REAL 2) st p in C holds ex i being Nat st ( i in dom S & p in Segm (S,i) ) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for p being Point of (TOP-REAL 2) st p in C holds ex i being Nat st ( i in dom S & p in Segm (S,i) ) let S be Segmentation of C; ::_thesis: for p being Point of (TOP-REAL 2) st p in C holds ex i being Nat st ( i in dom S & p in Segm (S,i) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies ex i being Nat st ( i in dom S & p in Segm (S,i) ) ) assume A1: p in C ; ::_thesis: ex i being Nat st ( i in dom S & p in Segm (S,i) ) set X = { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } ; A2: { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } c= dom S proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } or e in dom S ) assume e in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } ; ::_thesis: e in dom S then ex i being Element of NAT st ( e = i & i in dom S & LE S /. i,p,C ) ; hence e in dom S ; ::_thesis: verum end; A3: 1 in dom S by FINSEQ_5:6; A4: W-min C = S /. 1 by Def3; then LE S /. 1,p,C by A1, JORDAN7:3; then 1 in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } by A3; then reconsider X = { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } as non empty finite Subset of NAT by A2, XBOOLE_1:1; take max X ; ::_thesis: ( max X in dom S & p in Segm (S,(max X)) ) A5: max X in X by XXREAL_2:def_8; hence max X in dom S by A2; ::_thesis: p in Segm (S,(max X)) A6: 1 <= max X by A2, A5, FINSEQ_3:25; A7: max X <= len S by A2, A5, FINSEQ_3:25; A8: ex i being Element of NAT st ( max X = i & i in dom S & LE S /. i,p,C ) by A5; reconsider mX = max X as Element of NAT by ORDINAL1:def_12; percases ( max X < len S or max X = len S ) by A7, XXREAL_0:1; supposeA9: max X < len S ; ::_thesis: p in Segm (S,(max X)) A10: 1 <= (max X) + 1 by NAT_1:11; (max X) + 1 <= len S by A9, NAT_1:13; then A11: mX + 1 in dom S by A10, FINSEQ_3:25; A12: S is one-to-one by Def3; (max X) + 1 >= 1 + 1 by A6, XREAL_1:6; then (max X) + 1 <> 1 ; then A13: S /. ((max X) + 1) <> S /. 1 by A3, A11, A12, PARTFUN2:10; A14: S /. ((max X) + 1) in rng S by A11, PARTFUN2:2; A15: rng S c= C by Def3; now__::_thesis:_not_LE_S_/._((max_X)_+_1),p,C assume LE S /. ((max X) + 1),p,C ; ::_thesis: contradiction then (max X) + 1 in X by A11; then (max X) + 1 <= max X by XXREAL_2:def_8; hence contradiction by XREAL_1:29; ::_thesis: verum end; then LE p,S /. ((max X) + 1),C by A1, A14, A15, JORDAN16:7; then p in { p1 where p1 is Point of (TOP-REAL 2) : ( LE S /. (max X),p1,C & LE p1,S /. ((max X) + 1),C ) } by A8; then p in Segment ((S /. (max X)),(S /. ((max X) + 1)),C) by A4, A13, JORDAN7:def_1; hence p in Segm (S,(max X)) by A6, A9, Def4; ::_thesis: verum end; supposeA16: max X = len S ; ::_thesis: p in Segm (S,(max X)) now__::_thesis:_(_(_p_<>_W-min_C_&_LE_S_/._(len_S),p,C_)_or_(_p_=_W-min_C_&_S_/._(len_S)_in_C_)_) percases ( p <> W-min C or p = W-min C ) ; case p <> W-min C ; ::_thesis: LE S /. (len S),p,C thus LE S /. (len S),p,C by A8, A16; ::_thesis: verum end; case p = W-min C ; ::_thesis: S /. (len S) in C A17: S /. (len S) in rng S by REVROT_1:3; rng S c= C by Def3; hence S /. (len S) in C by A17; ::_thesis: verum end; end; end; then p in { p1 where p1 is Point of (TOP-REAL 2) : ( LE S /. (len S),p1,C or ( S /. (len S) in C & p1 = W-min C ) ) } ; then p in Segment ((S /. (len S)),(S /. 1),C) by A4, JORDAN7:def_1; hence p in Segm (S,(max X)) by A16, Def4; ::_thesis: verum end; end; end; theorem Th24: :: JORDAN_A:24 for C being Simple_closed_curve for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds Segm (S,i) misses Segm (S,j) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds Segm (S,i) misses Segm (S,j) let S be Segmentation of C; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds Segm (S,i) misses Segm (S,j) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 implies Segm (S,i) misses Segm (S,j) ) assume that A1: 1 <= i and A2: i < j and A3: j < len S and A4: not i,j are_adjacent1 ; ::_thesis: Segm (S,i) misses Segm (S,j) i < len S by A2, A3, XXREAL_0:2; then A5: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by A1, Def4; 1 < j by A1, A2, XXREAL_0:2; then Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A3, Def4; hence Segm (S,i) misses Segm (S,j) by A1, A2, A3, A4, A5, Def3; ::_thesis: verum end; theorem Th25: :: JORDAN_A:25 for C being Simple_closed_curve for S being Segmentation of C for j being Element of NAT st 1 < j & j < (len S) -' 1 holds Segm (S,(len S)) misses Segm (S,j) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for j being Element of NAT st 1 < j & j < (len S) -' 1 holds Segm (S,(len S)) misses Segm (S,j) let S be Segmentation of C; ::_thesis: for j being Element of NAT st 1 < j & j < (len S) -' 1 holds Segm (S,(len S)) misses Segm (S,j) let j be Element of NAT ; ::_thesis: ( 1 < j & j < (len S) -' 1 implies Segm (S,(len S)) misses Segm (S,j) ) assume that A1: 1 < j and A2: j < (len S) -' 1 ; ::_thesis: Segm (S,(len S)) misses Segm (S,j) A3: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4; A4: j + 1 < len S by A2, NAT_D:53; j < len S by A2, NAT_D:44; then Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A1, Def4; hence Segm (S,(len S)) misses Segm (S,j) by A1, A3, A4, Def3; ::_thesis: verum end; theorem Th26: :: JORDAN_A:26 for C being Simple_closed_curve for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} let S be Segmentation of C; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent1 implies (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} ) assume that A1: 1 <= i and A2: i < j and A3: j < len S and A4: i,j are_adjacent1 ; ::_thesis: (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} i < len S by A2, A3, XXREAL_0:2; then A5: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by A1, Def4; 1 < j by A1, A2, XXREAL_0:2; then A6: Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A3, Def4; j + 1 > i by A2, NAT_1:13; then j = i + 1 by A4, GOBRD10:def_1; then j + 1 = i + (1 + 1) ; hence (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} by A1, A3, A5, A6, Def3; ::_thesis: verum end; theorem Th27: :: JORDAN_A:27 for C being Simple_closed_curve for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds Segm (S,i) meets Segm (S,j) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds Segm (S,i) meets Segm (S,j) let S be Segmentation of C; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds Segm (S,i) meets Segm (S,j) let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent1 implies Segm (S,i) meets Segm (S,j) ) assume that A1: 1 <= i and A2: i < j and A3: j < len S and A4: i,j are_adjacent1 ; ::_thesis: Segm (S,i) meets Segm (S,j) (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} by A1, A2, A3, A4, Th26; hence Segm (S,i) meets Segm (S,j) by XBOOLE_0:def_7; ::_thesis: verum end; theorem Th28: :: JORDAN_A:28 for C being Simple_closed_curve for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} let S be Segmentation of C; ::_thesis: (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} A1: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4; len S >= 8 by Def3; then 1 < len S by XXREAL_0:2; then Segm (S,1) = Segment ((S /. 1),(S /. (1 + 1)),C) by Def4; hence (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} by A1, Def3; ::_thesis: verum end; theorem Th29: :: JORDAN_A:29 for C being Simple_closed_curve for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1) let S be Segmentation of C; ::_thesis: Segm (S,(len S)) meets Segm (S,1) (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} by Th28; hence Segm (S,(len S)) meets Segm (S,1) by XBOOLE_0:def_7; ::_thesis: verum end; theorem Th30: :: JORDAN_A:30 for C being Simple_closed_curve for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} let S be Segmentation of C; ::_thesis: (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} A1: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4; A2: len S >= 8 by Def3; then len S >= 1 + 1 by XXREAL_0:2; then A3: 1 <= (len S) -' 1 by NAT_D:55; A4: ((len S) -' 1) + 1 = len S by A2, XREAL_1:235, XXREAL_0:2; then (len S) -' 1 < len S by NAT_1:13; then Segm (S,((len S) -' 1)) = Segment ((S /. ((len S) -' 1)),(S /. (len S)),C) by A3, A4, Def4; hence (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} by A1, Def3; ::_thesis: verum end; theorem Th31: :: JORDAN_A:31 for C being Simple_closed_curve for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1)) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1)) let S be Segmentation of C; ::_thesis: Segm (S,(len S)) meets Segm (S,((len S) -' 1)) (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} by Th30; hence Segm (S,(len S)) meets Segm (S,((len S) -' 1)) by XBOOLE_0:def_7; ::_thesis: verum end; begin definition let n be Element of NAT ; let C be Subset of (TOP-REAL n); func diameter C -> Real means :Def5: :: JORDAN_A:def 5 ex W being Subset of (Euclid n) st ( W = C & it = diameter W ); existence ex b1 being Real ex W being Subset of (Euclid n) st ( W = C & b1 = diameter W ) proof TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8 .= TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) by PCOMPS_1:def_5 ; then reconsider W = C as Subset of (Euclid n) ; take diameter W ; ::_thesis: ex W being Subset of (Euclid n) st ( W = C & diameter W = diameter W ) take W ; ::_thesis: ( W = C & diameter W = diameter W ) thus ( W = C & diameter W = diameter W ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Real st ex W being Subset of (Euclid n) st ( W = C & b1 = diameter W ) & ex W being Subset of (Euclid n) st ( W = C & b2 = diameter W ) holds b1 = b2; ; end; :: deftheorem Def5 defines diameter JORDAN_A:def_5_:_ for n being Element of NAT for C being Subset of (TOP-REAL n) for b3 being Real holds ( b3 = diameter C iff ex W being Subset of (Euclid n) st ( W = C & b3 = diameter W ) ); definition let C be Simple_closed_curve; let S be Segmentation of C; func diameter S -> Real means :Def6: :: JORDAN_A:def 6 ex S1 being non empty finite Subset of REAL st ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & it = max S1 ); existence ex b1 being Real ex S1 being non empty finite Subset of REAL st ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b1 = max S1 ) proof deffunc H1( Element of NAT ) -> Real = diameter (Segm (S,$1)); defpred S1[ set ] means $1 in dom S; set S1 = { H1(i) where i is Element of NAT : S1[i] } ; set S2 = { H1(i) where i is Element of NAT : i in dom S } ; A1: dom S is finite ; A2: { H1(i) where i is Element of NAT : i in dom S } is finite from FRAENKEL:sch_21(A1); A3: { H1(i) where i is Element of NAT : S1[i] } is Subset of REAL from DOMAIN_1:sch_8(); 1 in dom S by FINSEQ_5:6; then diameter (Segm (S,1)) in { H1(i) where i is Element of NAT : S1[i] } ; then reconsider S1 = { H1(i) where i is Element of NAT : S1[i] } as non empty finite Subset of REAL by A2, A3; reconsider mS1 = max S1 as Element of REAL by XREAL_0:def_1; take mS1 ; ::_thesis: ex S1 being non empty finite Subset of REAL st ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 ) take S1 ; ::_thesis: ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 ) thus ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Real st ex S1 being non empty finite Subset of REAL st ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b1 = max S1 ) & ex S1 being non empty finite Subset of REAL st ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b2 = max S1 ) holds b1 = b2; ; end; :: deftheorem Def6 defines diameter JORDAN_A:def_6_:_ for C being Simple_closed_curve for S being Segmentation of C for b3 being Real holds ( b3 = diameter S iff ex S1 being non empty finite Subset of REAL st ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b3 = max S1 ) ); theorem :: JORDAN_A:32 for C being Simple_closed_curve for S being Segmentation of C for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S let S be Segmentation of C; ::_thesis: for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S let i be Element of NAT ; ::_thesis: diameter (Segm (S,i)) <= diameter S consider S1 being non empty finite Subset of REAL such that A1: S1 = { (diameter (Segm (S,j))) where j is Element of NAT : j in dom S } and A2: diameter S = max S1 by Def6; percases ( ( 1 <= i & i < len S ) or not 1 <= i or not i < len S ) ; suppose ( 1 <= i & i < len S ) ; ::_thesis: diameter (Segm (S,i)) <= diameter S then i in dom S by FINSEQ_3:25; then diameter (Segm (S,i)) in S1 by A1; hence diameter (Segm (S,i)) <= diameter S by A2, XXREAL_2:def_8; ::_thesis: verum end; supposeA3: ( not 1 <= i or not i < len S ) ; ::_thesis: diameter (Segm (S,i)) <= diameter S A4: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4 .= Segm (S,i) by A3, Def4 ; len S in dom S by FINSEQ_5:6; then diameter (Segm (S,i)) in S1 by A1, A4; hence diameter (Segm (S,i)) <= diameter S by A2, XXREAL_2:def_8; ::_thesis: verum end; end; end; theorem Th33: :: JORDAN_A:33 for C being Simple_closed_curve for S being Segmentation of C for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds diameter S < e proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds diameter S < e let S be Segmentation of C; ::_thesis: for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds diameter S < e let e be Real; ::_thesis: ( ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) implies diameter S < e ) assume A1: for i being Element of NAT holds diameter (Segm (S,i)) < e ; ::_thesis: diameter S < e consider S1 being non empty finite Subset of REAL such that A2: S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } and A3: diameter S = max S1 by Def6; diameter S in S1 by A3, XXREAL_2:def_8; then ex i being Element of NAT st ( diameter S = diameter (Segm (S,i)) & i in dom S ) by A2; hence diameter S < e by A1; ::_thesis: verum end; theorem :: JORDAN_A:34 for C being Simple_closed_curve for e being Real st e > 0 holds ex S being Segmentation of C st diameter S < e proof let C be Simple_closed_curve; ::_thesis: for e being Real st e > 0 holds ex S being Segmentation of C st diameter S < e let e be Real; ::_thesis: ( e > 0 implies ex S being Segmentation of C st diameter S < e ) assume e > 0 ; ::_thesis: ex S being Segmentation of C st diameter S < e then consider h being FinSequence of the carrier of (TOP-REAL 2) such that A1: h . 1 = W-min C and A2: h is one-to-one and A3: 8 <= len h and A4: rng h c= C and A5: for i being Element of NAT st 1 <= i & i < len h holds LE h /. i,h /. (i + 1),C and A6: for i being Element of NAT for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),C) holds diameter W < e and A7: for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),C) holds diameter W < e and A8: for i being Element of NAT st 1 <= i & i + 1 < len h holds (Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} and A9: (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} and A10: (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} and A11: Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) and A12: for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and A13: for i being Element of NAT st 1 < i & i + 1 < len h holds Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by JORDAN7:20; h <> {} by A3, CARD_1:27; then 1 in dom h by FINSEQ_5:6; then h /. 1 = W-min C by A1, PARTFUN1:def_6; then reconsider h = h as Segmentation of C by A2, A3, A4, A5, A8, A9, A10, A11, A12, A13, Def3; take h ; ::_thesis: diameter h < e for i being Element of NAT holds diameter (Segm (h,i)) < e proof let i be Element of NAT ; ::_thesis: diameter (Segm (h,i)) < e A14: ex W being Subset of (Euclid 2) st ( W = Segm (h,i) & diameter (Segm (h,i)) = diameter W ) by Def5; percases ( ( 1 <= i & i < len h ) or not 1 <= i or not i < len h ) ; supposeA15: ( 1 <= i & i < len h ) ; ::_thesis: diameter (Segm (h,i)) < e then Segm (h,i) = Segment ((h /. i),(h /. (i + 1)),C) by Def4; hence diameter (Segm (h,i)) < e by A6, A14, A15; ::_thesis: verum end; suppose ( not 1 <= i or not i < len h ) ; ::_thesis: diameter (Segm (h,i)) < e then Segm (h,i) = Segment ((h /. (len h)),(h /. 1),C) by Def4; hence diameter (Segm (h,i)) < e by A7, A14; ::_thesis: verum end; end; end; hence diameter h < e by Th33; ::_thesis: verum end; begin definition let C be Simple_closed_curve; let S be Segmentation of C; func S-Gap S -> Real means :Def7: :: JORDAN_A:def 7 ex S1, S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & it = min ((min S1),(min S2)) ); existence ex b1 being Real ex S1, S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min ((min S1),(min S2)) ) proof deffunc H1( Element of NAT ) -> Element of REAL = dist_min ((Segm (S,(len S))),(Segm (S,$1))); deffunc H2( Element of NAT , Element of NAT ) -> Element of REAL = dist_min ((Segm (S,$1)),(Segm (S,$2))); defpred S1[ Element of NAT ] means ( 1 < $1 & $1 < (len S) -' 1 ); defpred S2[ Element of NAT ] means $1 in dom S; defpred S3[ Element of NAT , Element of NAT ] means ( 1 <= $1 & $1 < $2 & $2 < len S & not $1,$2 are_adjacent1 ); defpred S4[ Element of NAT , Element of NAT ] means ( S2[$1] & S2[$2] ); set S1 = { H2(i,j) where i, j is Element of NAT : S3[i,j] } ; set S2 = { H1(j) where j is Element of NAT : S1[j] } ; set B = { H2(i,j) where i, j is Element of NAT : S4[i,j] } ; set B9 = { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } ; set A = { H1(j) where j is Element of NAT : S2[j] } ; set A9 = { H1(j) where j is Element of NAT : j in dom S } ; A1: for j being Element of NAT st S1[j] holds S2[j] proof let j be Element of NAT ; ::_thesis: ( S1[j] implies S2[j] ) assume A2: 1 < j ; ::_thesis: ( not j < (len S) -' 1 or S2[j] ) A3: (len S) -' 1 <= len S by NAT_D:35; assume j < (len S) -' 1 ; ::_thesis: S2[j] then j < len S by A3, XXREAL_0:2; hence S2[j] by A2, FINSEQ_3:25; ::_thesis: verum end; A4: { H1(j) where j is Element of NAT : S1[j] } c= { H1(j) where j is Element of NAT : S2[j] } from FRAENKEL:sch_1(A1); A5: for i, j being Element of NAT st S3[i,j] holds S4[i,j] proof let i, j be Element of NAT ; ::_thesis: ( S3[i,j] implies S4[i,j] ) assume that A6: 1 <= i and A7: i < j and A8: j < len S and not i,j are_adjacent1 ; ::_thesis: S4[i,j] i < len S by A7, A8, XXREAL_0:2; hence i in dom S by A6, FINSEQ_3:25; ::_thesis: S2[j] 1 < j by A6, A7, XXREAL_0:2; hence S2[j] by A8, FINSEQ_3:25; ::_thesis: verum end; A9: { H2(i,j) where i, j is Element of NAT : S3[i,j] } c= { H2(i,j) where i, j is Element of NAT : S4[i,j] } from FRAENKEL:sch_2(A5); A10: { H2(i,j) where i, j is Element of NAT : S3[i,j] } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H2(i,j) where i, j is Element of NAT : S3[i,j] } or x in REAL ) assume x in { H2(i,j) where i, j is Element of NAT : S3[i,j] } ; ::_thesis: x in REAL then ex i, j being Element of NAT st ( x = dist_min ((Segm (S,i)),(Segm (S,j))) & 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) ; hence x in REAL ; ::_thesis: verum end; A11: { H1(j) where j is Element of NAT : S1[j] } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(j) where j is Element of NAT : S1[j] } or x in REAL ) assume x in { H1(j) where j is Element of NAT : S1[j] } ; ::_thesis: x in REAL then ex j being Element of NAT st ( x = dist_min ((Segm (S,(len S))),(Segm (S,j))) & 1 < j & j < (len S) -' 1 ) ; hence x in REAL ; ::_thesis: verum end; A12: dom S is finite ; A13: { H1(j) where j is Element of NAT : j in dom S } is finite from FRAENKEL:sch_21(A12); A14: { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } is finite from FRAENKEL:sch_22(A12, A12); A15: 3 <> 1 + 1 ; 1 <> 3 + 1 ; then A16: not 1,3 are_adjacent1 by A15, GOBRD10:def_1; A17: len S >= 7 + 1 by Def3; then 3 < len S by XXREAL_0:2; then A18: dist_min ((Segm (S,1)),(Segm (S,3))) in { H2(i,j) where i, j is Element of NAT : S3[i,j] } by A16; 2 + 1 < len S by A17, XXREAL_0:2; then 2 < (len S) -' 1 by NAT_D:52; then dist_min ((Segm (S,(len S))),(Segm (S,2))) in { H1(j) where j is Element of NAT : S1[j] } ; then reconsider S1 = { H2(i,j) where i, j is Element of NAT : S3[i,j] } , S2 = { H1(j) where j is Element of NAT : S1[j] } as non empty finite Subset of REAL by A4, A9, A10, A11, A13, A14, A18; reconsider mm = min ((min S1),(min S2)) as Element of REAL by XREAL_0:def_1; take mm ; ::_thesis: ex S1, S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) ) take S1 ; ::_thesis: ex S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) ) take S2 ; ::_thesis: ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) ) thus ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being Real st ex S1, S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min ((min S1),(min S2)) ) & ex S1, S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b2 = min ((min S1),(min S2)) ) holds b1 = b2; ; end; :: deftheorem Def7 defines S-Gap JORDAN_A:def_7_:_ for C being Simple_closed_curve for S being Segmentation of C for b3 being Real holds ( b3 = S-Gap S iff ex S1, S2 being non empty finite Subset of REAL st ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b3 = min ((min S1),(min S2)) ) ); theorem Th35: :: JORDAN_A:35 for C being Simple_closed_curve for S being Segmentation of C ex F being non empty finite Subset of REAL st ( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F ) proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C ex F being non empty finite Subset of REAL st ( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F ) let S be Segmentation of C; ::_thesis: ex F being non empty finite Subset of REAL st ( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F ) consider S1, S2 being non empty finite Subset of REAL such that A1: S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } and A2: S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } and A3: S-Gap S = min ((min S1),(min S2)) by Def7; take F = S1 \/ S2; ::_thesis: ( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F ) set X = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } ; thus F c= { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } :: according to XBOOLE_0:def_10 ::_thesis: ( { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } c= F & S-Gap S = min F ) proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F or e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } ) assume A4: e in F ; ::_thesis: e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } percases ( e in S1 or e in S2 ) by A4, XBOOLE_0:def_3; suppose e in S1 ; ::_thesis: e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } then consider i, j being Element of NAT such that A5: e = dist_min ((Segm (S,i)),(Segm (S,j))) and A6: 1 <= i and A7: i < j and A8: j < len S and A9: not i,j are_adjacent1 by A1; Segm (S,i) misses Segm (S,j) by A6, A7, A8, A9, Th24; hence e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } by A5, A6, A7, A8; ::_thesis: verum end; suppose e in S2 ; ::_thesis: e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } then consider j being Element of NAT such that A10: e = dist_min ((Segm (S,(len S))),(Segm (S,j))) and A11: 1 < j and A12: j < (len S) -' 1 by A2; A13: j < len S by A12, NAT_D:44; Segm (S,(len S)) misses Segm (S,j) by A11, A12, Th25; hence e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } by A10, A11, A13; ::_thesis: verum end; end; end; thus { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } c= F ::_thesis: S-Gap S = min F proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } or e in F ) assume e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } ; ::_thesis: e in F then consider i, j being Element of NAT such that A14: e = dist_min ((Segm (S,i)),(Segm (S,j))) and A15: 1 <= i and A16: i < j and A17: j <= len S and A18: Segm (S,i) misses Segm (S,j) ; A19: i < len S by A16, A17, XXREAL_0:2; percases ( j < len S or j = len S ) by A17, XXREAL_0:1; supposeA20: j < len S ; ::_thesis: e in F not i,j are_adjacent1 by A15, A16, A18, A20, Th27; then e in S1 by A1, A14, A15, A16, A20; hence e in F by XBOOLE_0:def_3; ::_thesis: verum end; supposeA21: j = len S ; ::_thesis: e in F then 1 <> i by A18, Th29; then A22: 1 < i by A15, XXREAL_0:1; A23: i <= (len S) -' 1 by A19, NAT_D:49; i <> (len S) -' 1 by A18, A21, Th31; then i < (len S) -' 1 by A23, XXREAL_0:1; then e in S2 by A2, A14, A21, A22; hence e in F by XBOOLE_0:def_3; ::_thesis: verum end; end; end; thus S-Gap S = min F by A3, XXREAL_2:9; ::_thesis: verum end; theorem :: JORDAN_A:36 for C being Simple_closed_curve for S being Segmentation of C holds S-Gap S > 0 proof let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds S-Gap S > 0 let S be Segmentation of C; ::_thesis: S-Gap S > 0 consider F being non empty finite Subset of REAL such that A1: F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } and A2: S-Gap S = min F by Th35; S-Gap S in F by A2, XXREAL_2:def_7; then ex i, j being Element of NAT st ( S-Gap S = dist_min ((Segm (S,i)),(Segm (S,j))) & 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) by A1; hence S-Gap S > 0 by Th7; ::_thesis: verum end;