:: JORDAN5C semantic presentation begin theorem Th1: :: JORDAN5C:1 for P, Q being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q let s1 be Real; ::_thesis: ( q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds not f . t in Q ) implies for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) assume that A1: q1 in P and A2: f . s1 = q1 and A3: f is being_homeomorphism and A4: f . 0 = p1 and A5: f . 1 = p2 and A6: ( 0 <= s1 & s1 <= 1 ) and A7: for t being Real st 0 <= t & t < s1 holds not f . t in Q ; ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1; let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds not g . t in Q ) assume that A8: g is being_homeomorphism and A9: g . 0 = p1 and A10: g . 1 = p2 and A11: g . s2 = q1 and A12: 0 <= s2 and A13: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds not g . t in Q reconsider f = f, g = g as Function of I[01],((TOP-REAL 2) | P9) ; A14: f is one-to-one by A3, TOPS_2:def_5; A15: dom f = [#] I[01] by A3, TOPS_2:def_5; then A16: 1 in dom f by BORSUK_1:43; A17: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def_5; then f is onto by FUNCT_2:def_3; then A18: f " = f " by A14, TOPS_2:def_4; A19: (f ") . p2 = 1 by A5, A16, A14, A18, FUNCT_1:32; A20: 0 in dom f by A15, BORSUK_1:43; A21: (f ") . p1 = 0 by A4, A20, A14, A18, FUNCT_1:32; set fg = (f ") * g; A22: f " is being_homeomorphism by A3, TOPS_2:56; then (f ") * g is being_homeomorphism by A8, TOPS_2:57; then A23: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def_5; let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in Q ) assume that A24: 0 <= t and A25: t < s2 ; ::_thesis: not g . t in Q A26: t <= 1 by A13, A25, XXREAL_0:2; then reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A24, BORSUK_1:43; A27: t in the carrier of I[01] by A24, A26, BORSUK_1:43; then ((f ") * g) . t in the carrier of I[01] by FUNCT_2:5; then reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40; A28: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def_5; A29: dom g = [#] I[01] by A8, TOPS_2:def_5; then 1 in dom g by BORSUK_1:43; then A30: ((f ") * g) . 1 = 1 by A10, A19, FUNCT_1:13; A31: s1 in dom f by A6, A15, BORSUK_1:43; dom (f ") = [#] ((TOP-REAL 2) | P) by A22, TOPS_2:def_5; then A32: dom ((f ") * g) = dom g by A28, RELAT_1:27; 0 in dom g by A29, BORSUK_1:43; then A33: ((f ") * g) . 0 = 0 by A9, A21, FUNCT_1:13; A34: 0 <= Ft proof percases ( 0 < t or 0 = t ) by A24; suppose 0 < t ; ::_thesis: 0 <= Ft hence 0 <= Ft by A23, A33, A30, BORSUK_1:def_14, JORDAN5A:15, TOPMETR:20; ::_thesis: verum end; suppose 0 = t ; ::_thesis: 0 <= Ft hence 0 <= Ft by A9, A21, A29, FUNCT_1:13; ::_thesis: verum end; end; end; f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36 .= g * (id (rng f)) by A17, A14, TOPS_2:52 .= (id (rng g)) * g by A8, A17, TOPS_2:def_5 .= g by RELAT_1:54 ; then A35: f . (((f ") * g) . t) = g . t by A29, A27, A32, FUNCT_1:13; s2 in dom g by A12, A13, A29, BORSUK_1:43; then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:13 .= s1 by A2, A14, A31, A18, FUNCT_1:32 ; then ((f ") * g) . s29 = s1 ; then Ft < s1 by A25, A23, A33, A30, JORDAN5A:15, TOPMETR:20; hence not g . t in Q by A7, A34, A35; ::_thesis: verum end; definition let P, Q be Subset of (TOP-REAL 2); let p1, p2 be Point of (TOP-REAL 2); assume that A1: ( P meets Q & P /\ Q is closed ) and A2: P is_an_arc_of p1,p2 ; func First_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN5C:def 1 ( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ); existence ex b1 being Point of (TOP-REAL 2) st ( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) proof consider EX being Point of (TOP-REAL 2) such that A3: EX in P /\ Q and A4: ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) by A1, A2, JORDAN5A:21; EX in P by A3, XBOOLE_0:def_4; then for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q by A4, Th1; hence ex b1 being Point of (TOP-REAL 2) st ( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) holds b1 = b2 proof let IT1, IT2 be Point of (TOP-REAL 2); ::_thesis: ( IT1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) & IT2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) implies IT1 = IT2 ) A5: P /\ Q c= Q by XBOOLE_1:17; A6: P /\ Q c= P by XBOOLE_1:17; assume that A7: IT1 in P /\ Q and A8: for g1 being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st g1 is being_homeomorphism & g1 . 0 = p1 & g1 . 1 = p2 & g1 . s1 = IT1 & 0 <= s1 & s1 <= 1 holds for t being Real st 0 <= t & t < s1 holds not g1 . t in Q ; ::_thesis: ( not IT2 in P /\ Q or ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 & ex t being Real st ( 0 <= t & t < s2 & g . t in Q ) ) or IT1 = IT2 ) assume that A9: IT2 in P /\ Q and A10: for g2 being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g2 is being_homeomorphism & g2 . 0 = p1 & g2 . 1 = p2 & g2 . s2 = IT2 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g2 . t in Q ; ::_thesis: IT1 = IT2 consider g being Function of I[01],((TOP-REAL 2) | P) such that A11: g is being_homeomorphism and A12: ( g . 0 = p1 & g . 1 = p2 ) by A2, TOPREAL1:def_1; A13: rng g = [#] ((TOP-REAL 2) | P) by A11, TOPS_2:def_5 .= P by PRE_TOPC:def_5 ; then consider ss1 being set such that A14: ss1 in dom g and A15: g . ss1 = IT1 by A6, A7, FUNCT_1:def_3; A16: dom g = [#] I[01] by A11, TOPS_2:def_5 .= the carrier of I[01] ; then reconsider ss1 = ss1 as Real by A14, BORSUK_1:40; A17: 0 <= ss1 by A14, BORSUK_1:43; consider ss2 being set such that A18: ss2 in dom g and A19: g . ss2 = IT2 by A6, A9, A13, FUNCT_1:def_3; reconsider ss2 = ss2 as Real by A16, A18, BORSUK_1:40; A20: 0 <= ss2 by A18, BORSUK_1:43; A21: ss1 <= 1 by A14, BORSUK_1:43; A22: ss2 <= 1 by A18, BORSUK_1:43; percases ( ss1 < ss2 or ss1 = ss2 or ss1 > ss2 ) by XXREAL_0:1; suppose ss1 < ss2 ; ::_thesis: IT1 = IT2 hence IT1 = IT2 by A5, A7, A10, A11, A12, A15, A19, A17, A22; ::_thesis: verum end; suppose ss1 = ss2 ; ::_thesis: IT1 = IT2 hence IT1 = IT2 by A15, A19; ::_thesis: verum end; suppose ss1 > ss2 ; ::_thesis: IT1 = IT2 hence IT1 = IT2 by A5, A8, A9, A11, A12, A15, A19, A21, A20; ::_thesis: verum end; end; end; end; :: deftheorem Def1 defines First_Point JORDAN5C:def_1_:_ for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds for b5 being Point of (TOP-REAL 2) holds ( b5 = First_Point (P,p1,p2,Q) iff ( b5 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q ) ) ); theorem :: JORDAN5C:2 for P, Q being Subset of (TOP-REAL 2) for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds First_Point (P,p1,p2,Q) = p proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds First_Point (P,p1,p2,Q) = p let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies First_Point (P,p1,p2,Q) = p ) assume that A1: p in P and A2: P is_an_arc_of p1,p2 and A3: Q = {p} ; ::_thesis: First_Point (P,p1,p2,Q) = p A4: P /\ {p} = {p} by A1, ZFMISC_1:46; A5: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in {p} proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in {p} let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds not g . t in {p} ) assume that A6: g is being_homeomorphism and g . 0 = p1 and g . 1 = p2 and A7: g . s2 = p and A8: 0 <= s2 and A9: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds not g . t in {p} A10: g is one-to-one by A6, TOPS_2:def_5; let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in {p} ) assume that A11: 0 <= t and A12: t < s2 ; ::_thesis: not g . t in {p} A13: dom g = the carrier of I[01] by A1, FUNCT_2:def_1; t <= 1 by A9, A12, XXREAL_0:2; then A14: t in dom g by A13, A11, BORSUK_1:43; s2 in dom g by A8, A9, A13, BORSUK_1:43; then g . t <> g . s2 by A10, A12, A14, FUNCT_1:def_4; hence not g . t in {p} by A7, TARSKI:def_1; ::_thesis: verum end; A15: P /\ Q is closed by A3, A4, PCOMPS_1:7; A16: p in P /\ {p} by A4, TARSKI:def_1; then P meets {p} by A1, A4, XBOOLE_0:3; hence First_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def1; ::_thesis: verum end; theorem Th3: :: JORDAN5C:3 for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds First_Point (P,p1,p2,Q) = p1 proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds First_Point (P,p1,p2,Q) = p1 let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies First_Point (P,p1,p2,Q) = p1 ) assume that A1: p1 in Q and A2: P /\ Q is closed and A3: P is_an_arc_of p1,p2 ; ::_thesis: First_Point (P,p1,p2,Q) = p1 A4: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds not g . t in Q ) assume that A5: g is being_homeomorphism and A6: g . 0 = p1 and g . 1 = p2 and A7: g . s2 = p1 and A8: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: for t being Real st 0 <= t & t < s2 holds not g . t in Q A9: g is one-to-one by A5, TOPS_2:def_5; let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in Q ) assume A10: ( 0 <= t & t < s2 ) ; ::_thesis: not g . t in Q A11: dom g = [#] I[01] by A5, TOPS_2:def_5 .= the carrier of I[01] ; then A12: 0 in dom g by BORSUK_1:43; s2 in dom g by A8, A11, BORSUK_1:43; hence not g . t in Q by A6, A7, A12, A9, A10, FUNCT_1:def_4; ::_thesis: verum end; p1 in P by A3, TOPREAL1:1; then ( p1 in P /\ Q & P meets Q ) by A1, XBOOLE_0:3, XBOOLE_0:def_4; hence First_Point (P,p1,p2,Q) = p1 by A2, A3, A4, Def1; ::_thesis: verum end; theorem Th4: :: JORDAN5C:4 for P, Q being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds not f . t in Q ) holds for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q let s1 be Real; ::_thesis: ( q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds not f . t in Q ) implies for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) assume that A1: q1 in P and A2: f . s1 = q1 and A3: f is being_homeomorphism and A4: f . 0 = p1 and A5: f . 1 = p2 and A6: ( 0 <= s1 & s1 <= 1 ) and A7: for t being Real st 1 >= t & t > s1 holds not f . t in Q ; ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1; let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds not g . t in Q ) assume that A8: g is being_homeomorphism and A9: g . 0 = p1 and A10: g . 1 = p2 and A11: g . s2 = q1 and A12: 0 <= s2 and A13: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds not g . t in Q reconsider f = f, g = g as Function of I[01],((TOP-REAL 2) | P9) ; A14: f is one-to-one by A3, TOPS_2:def_5; set fg = (f ") * g; let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in Q ) assume that A15: 1 >= t and A16: t > s2 ; ::_thesis: not g . t in Q reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A15, A16, BORSUK_1:43; A17: t in the carrier of I[01] by A12, A15, A16, BORSUK_1:43; then ((f ") * g) . t in the carrier of I[01] by FUNCT_2:5; then reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40; A18: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def_5; A19: f " is being_homeomorphism by A3, TOPS_2:56; then (f ") * g is being_homeomorphism by A8, TOPS_2:57; then A20: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def_5; A21: dom f = [#] I[01] by A3, TOPS_2:def_5; then A22: 0 in dom f by BORSUK_1:43; A23: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def_5; then f is onto by FUNCT_2:def_3; then A24: f " = f " by A14, TOPS_2:def_4; then A25: (f ") . p1 = 0 by A4, A22, A14, FUNCT_1:32; A26: 1 in dom f by A21, BORSUK_1:43; A27: (f ") . p2 = 1 by A24, A5, A26, A14, FUNCT_1:32; A28: dom g = [#] I[01] by A8, TOPS_2:def_5; then 0 in dom g by BORSUK_1:43; then A29: ((f ") * g) . 0 = 0 by A9, A25, FUNCT_1:13; 1 in dom g by A28, BORSUK_1:43; then A30: ((f ") * g) . 1 = 1 by A10, A27, FUNCT_1:13; A31: Ft <= 1 proof percases ( t < 1 or t = 1 ) by A15, XXREAL_0:1; suppose t < 1 ; ::_thesis: Ft <= 1 hence Ft <= 1 by A20, A29, A30, BORSUK_1:def_15, JORDAN5A:15, TOPMETR:20; ::_thesis: verum end; suppose t = 1 ; ::_thesis: Ft <= 1 hence Ft <= 1 by A10, A27, A28, FUNCT_1:13; ::_thesis: verum end; end; end; dom (f ") = [#] ((TOP-REAL 2) | P) by A19, TOPS_2:def_5; then A32: t in dom ((f ") * g) by A28, A18, A17, RELAT_1:27; f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36 .= g * (id (rng f)) by A23, A14, TOPS_2:52 .= (id (rng g)) * g by A8, A23, TOPS_2:def_5 .= g by RELAT_1:54 ; then A33: f . (((f ") * g) . t) = g . t by A32, FUNCT_1:13; A34: s1 in dom f by A6, A21, BORSUK_1:43; s2 in dom g by A12, A13, A28, BORSUK_1:43; then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:13 .= s1 by A2, A14, A34, A24, FUNCT_1:32 ; then ((f ") * g) . s29 = s1 ; then s1 < Ft by A16, A20, A29, A30, JORDAN5A:15, TOPMETR:20; hence not g . t in Q by A7, A31, A33; ::_thesis: verum end; definition let P, Q be Subset of (TOP-REAL 2); let p1, p2 be Point of (TOP-REAL 2); assume that A1: ( P meets Q & P /\ Q is closed ) and A2: P is_an_arc_of p1,p2 ; func Last_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN5C:def 2 ( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ); existence ex b1 being Point of (TOP-REAL 2) st ( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) proof consider EX being Point of (TOP-REAL 2) such that A3: EX in P /\ Q and A4: ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) by A1, A2, JORDAN5A:22; EX in P by A3, XBOOLE_0:def_4; then for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q by A4, Th4; hence ex b1 being Point of (TOP-REAL 2) st ( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) holds b1 = b2 proof let IT1, IT2 be Point of (TOP-REAL 2); ::_thesis: ( IT1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT1 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) & IT2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) implies IT1 = IT2 ) A5: P /\ Q c= P by XBOOLE_1:17; assume that A6: IT1 in P /\ Q and A7: for g1 being Function of I[01],((TOP-REAL 2) | P) for s1 being Real st g1 is being_homeomorphism & g1 . 0 = p1 & g1 . 1 = p2 & g1 . s1 = IT1 & 0 <= s1 & s1 <= 1 holds for t being Real st 1 >= t & t > s1 holds not g1 . t in Q ; ::_thesis: ( not IT2 in P /\ Q or ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 & ex t being Real st ( 1 >= t & t > s2 & g . t in Q ) ) or IT1 = IT2 ) assume that A8: IT2 in P /\ Q and A9: for g2 being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g2 is being_homeomorphism & g2 . 0 = p1 & g2 . 1 = p2 & g2 . s2 = IT2 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g2 . t in Q ; ::_thesis: IT1 = IT2 consider g being Function of I[01],((TOP-REAL 2) | P) such that A10: g is being_homeomorphism and A11: ( g . 0 = p1 & g . 1 = p2 ) by A2, TOPREAL1:def_1; A12: rng g = [#] ((TOP-REAL 2) | P) by A10, TOPS_2:def_5 .= P by PRE_TOPC:def_5 ; then consider ss1 being set such that A13: ss1 in dom g and A14: g . ss1 = IT1 by A5, A6, FUNCT_1:def_3; A15: dom g = [#] I[01] by A10, TOPS_2:def_5 .= the carrier of I[01] ; then reconsider ss1 = ss1 as Real by A13, BORSUK_1:40; A16: 0 <= ss1 by A13, BORSUK_1:43; A17: ( P /\ Q c= Q & ss1 <= 1 ) by A13, BORSUK_1:43, XBOOLE_1:17; consider ss2 being set such that A18: ss2 in dom g and A19: g . ss2 = IT2 by A5, A8, A12, FUNCT_1:def_3; reconsider ss2 = ss2 as Real by A15, A18, BORSUK_1:40; A20: 0 <= ss2 by A18, BORSUK_1:43; A21: ss2 <= 1 by A18, BORSUK_1:43; percases ( ss1 < ss2 or ss1 = ss2 or ss1 > ss2 ) by XXREAL_0:1; suppose ss1 < ss2 ; ::_thesis: IT1 = IT2 hence IT1 = IT2 by A7, A8, A10, A11, A14, A19, A16, A17, A21; ::_thesis: verum end; suppose ss1 = ss2 ; ::_thesis: IT1 = IT2 hence IT1 = IT2 by A14, A19; ::_thesis: verum end; suppose ss1 > ss2 ; ::_thesis: IT1 = IT2 hence IT1 = IT2 by A6, A9, A10, A11, A14, A19, A17, A20, A21; ::_thesis: verum end; end; end; end; :: deftheorem Def2 defines Last_Point JORDAN5C:def_2_:_ for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds for b5 being Point of (TOP-REAL 2) holds ( b5 = Last_Point (P,p1,p2,Q) iff ( b5 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q ) ) ); theorem :: JORDAN5C:5 for P, Q being Subset of (TOP-REAL 2) for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds Last_Point (P,p1,p2,Q) = p proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds Last_Point (P,p1,p2,Q) = p let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies Last_Point (P,p1,p2,Q) = p ) assume that A1: p in P and A2: P is_an_arc_of p1,p2 and A3: Q = {p} ; ::_thesis: Last_Point (P,p1,p2,Q) = p A4: P /\ {p} = {p} by A1, ZFMISC_1:46; A5: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in {p} proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in {p} let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds not g . t in {p} ) assume that A6: g is being_homeomorphism and g . 0 = p1 and g . 1 = p2 and A7: g . s2 = p and A8: 0 <= s2 and A9: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds not g . t in {p} A10: g is one-to-one by A6, TOPS_2:def_5; A11: dom g = the carrier of I[01] by A1, FUNCT_2:def_1; then A12: s2 in dom g by A8, A9, BORSUK_1:43; let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in {p} ) assume that A13: 1 >= t and A14: t > s2 ; ::_thesis: not g . t in {p} t in dom g by A8, A11, A13, A14, BORSUK_1:43; then g . t <> g . s2 by A10, A14, A12, FUNCT_1:def_4; hence not g . t in {p} by A7, TARSKI:def_1; ::_thesis: verum end; A15: P /\ Q is closed by A3, A4, PCOMPS_1:7; A16: p in P /\ {p} by A4, TARSKI:def_1; then P meets {p} by A1, A4, XBOOLE_0:3; hence Last_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def2; ::_thesis: verum end; theorem Th6: :: JORDAN5C:6 for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds Last_Point (P,p1,p2,Q) = p2 proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds Last_Point (P,p1,p2,Q) = p2 let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies Last_Point (P,p1,p2,Q) = p2 ) assume that A1: p2 in Q and A2: P /\ Q is closed and A3: P is_an_arc_of p1,p2 ; ::_thesis: Last_Point (P,p1,p2,Q) = p2 A4: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds not g . t in Q ) assume that A5: g is being_homeomorphism and g . 0 = p1 and A6: ( g . 1 = p2 & g . s2 = p2 ) and A7: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: for t being Real st 1 >= t & t > s2 holds not g . t in Q A8: g is one-to-one by A5, TOPS_2:def_5; let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in Q ) assume A9: ( 1 >= t & t > s2 ) ; ::_thesis: not g . t in Q A10: dom g = [#] I[01] by A5, TOPS_2:def_5 .= the carrier of I[01] ; then A11: 1 in dom g by BORSUK_1:43; s2 in dom g by A7, A10, BORSUK_1:43; hence not g . t in Q by A6, A11, A8, A9, FUNCT_1:def_4; ::_thesis: verum end; p2 in P by A3, TOPREAL1:1; then ( p2 in P /\ Q & P meets Q ) by A1, XBOOLE_0:3, XBOOLE_0:def_4; hence Last_Point (P,p1,p2,Q) = p2 by A2, A3, A4, Def2; ::_thesis: verum end; theorem Th7: :: JORDAN5C:7 for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P c= Q & P is closed & P is_an_arc_of p1,p2 implies ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) ) assume that A1: P c= Q and A2: P is closed and A3: P is_an_arc_of p1,p2 ; ::_thesis: ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) A4: p2 in P by A3, TOPREAL1:1; ( P /\ Q = P & p1 in P ) by A1, A3, TOPREAL1:1, XBOOLE_1:28; hence ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) by A1, A2, A3, A4, Th3, Th6; ::_thesis: verum end; begin definition let P be Subset of (TOP-REAL 2); let p1, p2, q1, q2 be Point of (TOP-REAL 2); pred LE q1,q2,P,p1,p2 means :Def3: :: JORDAN5C:def 3 ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ); end; :: deftheorem Def3 defines LE JORDAN5C:def_3_:_ for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds ( LE q1,q2,P,p1,p2 iff ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ) ); theorem Th8: :: JORDAN5C:8 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds LE q1,q2,P,p1,p2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds LE q1,q2,P,p1,p2 let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds LE q1,q2,P,p1,p2 let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds LE q1,q2,P,p1,p2 let s1, s2 be Real; ::_thesis: ( P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 implies LE q1,q2,P,p1,p2 ) assume that A1: P is_an_arc_of p1,p2 and A2: g is being_homeomorphism and A3: g . 0 = p1 and A4: g . 1 = p2 and A5: g . s1 = q1 and A6: ( 0 <= s1 & s1 <= 1 ) and A7: g . s2 = q2 and A8: ( 0 <= s2 & s2 <= 1 ) and A9: s1 <= s2 ; ::_thesis: LE q1,q2,P,p1,p2 reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1; A10: s1 in the carrier of I[01] by A6, BORSUK_1:43; then A11: q1 in [#] ((TOP-REAL 2) | P9) by A5, FUNCT_2:5; reconsider g = g as Function of I[01],((TOP-REAL 2) | P9) ; A12: s2 in the carrier of I[01] by A8, BORSUK_1:43; then g . s2 in the carrier of ((TOP-REAL 2) | P9) by FUNCT_2:5; then A13: q2 in P by A7, A11, PRE_TOPC:def_5; A14: now__::_thesis:_for_h_being_Function_of_I[01],((TOP-REAL_2)_|_P9) for_t1,_t2_being_Real_st_h_is_being_homeomorphism_&_h_._0_=_p1_&_h_._1_=_p2_&_h_._t1_=_q1_&_0_<=_t1_&_t1_<=_1_&_h_._t2_=_q2_&_0_<=_t2_&_t2_<=_1_holds_ t1_<=_t2 reconsider s19 = s1, s29 = s2 as Point of I[01] by A6, A8, BORSUK_1:43; let h be Function of I[01],((TOP-REAL 2) | P9); ::_thesis: for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds b4 <= b5 let t1, t2 be Real; ::_thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 implies b2 <= b3 ) assume that A15: h is being_homeomorphism and A16: h . 0 = p1 and A17: h . 1 = p2 and A18: h . t1 = q1 and A19: ( 0 <= t1 & t1 <= 1 ) and A20: h . t2 = q2 and A21: ( 0 <= t2 & t2 <= 1 ) ; ::_thesis: b2 <= b3 A22: h is one-to-one by A15, TOPS_2:def_5; set hg = (h ") * g; h " is being_homeomorphism by A15, TOPS_2:56; then (h ") * g is being_homeomorphism by A2, TOPS_2:57; then A23: ( (h ") * g is continuous & (h ") * g is one-to-one ) by TOPS_2:def_5; ( ((h ") * g) . s1 in the carrier of I[01] & ((h ") * g) . s2 in the carrier of I[01] ) by A10, A12, FUNCT_2:5; then reconsider hg1 = ((h ") * g) . s19, hg2 = ((h ") * g) . s29 as Real by BORSUK_1:40; A24: dom g = [#] I[01] by A2, TOPS_2:def_5; then A25: 0 in dom g by BORSUK_1:43; A26: dom h = [#] I[01] by A15, TOPS_2:def_5; then A27: t1 in dom h by A19, BORSUK_1:43; A28: 0 in dom h by A26, BORSUK_1:43; rng h = [#] ((TOP-REAL 2) | P) by A15, TOPS_2:def_5; then h is onto by FUNCT_2:def_3; then A29: h " = h " by A22, TOPS_2:def_4; then (h ") . p1 = 0 by A16, A28, A22, FUNCT_1:32; then A30: ((h ") * g) . 0 = 0 by A3, A25, FUNCT_1:13; s1 in dom g by A6, A24, BORSUK_1:43; then A31: ((h ") * g) . s1 = (h ") . q1 by A5, FUNCT_1:13 .= t1 by A18, A22, A27, A29, FUNCT_1:32 ; A32: t2 in dom h by A21, A26, BORSUK_1:43; s2 in dom g by A8, A24, BORSUK_1:43; then A33: ((h ") * g) . s2 = (h ") . q2 by A7, FUNCT_1:13 .= t2 by A20, A22, A32, A29, FUNCT_1:32 ; A34: 1 in dom g by A24, BORSUK_1:43; A35: 1 in dom h by A26, BORSUK_1:43; (h ") . p2 = 1 by A17, A35, A22, A29, FUNCT_1:32; then A36: ((h ") * g) . 1 = 1 by A4, A34, FUNCT_1:13; percases ( s1 < s2 or s1 = s2 ) by A9, XXREAL_0:1; suppose s1 < s2 ; ::_thesis: b2 <= b3 then hg1 < hg2 by A23, A30, A36, JORDAN5A:16; hence t1 <= t2 by A31, A33; ::_thesis: verum end; suppose s1 = s2 ; ::_thesis: b2 <= b3 hence t1 <= t2 by A31, A33; ::_thesis: verum end; end; end; q1 in P by A11, PRE_TOPC:def_5; hence LE q1,q2,P,p1,p2 by A13, A14, Def3; ::_thesis: verum end; theorem Th9: :: JORDAN5C:9 for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds LE q1,q1,P,p1,p2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds LE q1,q1,P,p1,p2 let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( q1 in P implies LE q1,q1,P,p1,p2 ) assume A1: q1 in P ; ::_thesis: LE q1,q1,P,p1,p2 then reconsider P = P as non empty Subset of (TOP-REAL 2) ; now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P) for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_q1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_q1_&_0_<=_s2_&_s2_<=_1_holds_ s1_<=_s2 let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A2: g is being_homeomorphism and g . 0 = p1 and g . 1 = p2 and A3: g . s1 = q1 and A4: ( 0 <= s1 & s1 <= 1 ) and A5: g . s2 = q1 and A6: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 A7: g is one-to-one by A2, TOPS_2:def_5; ( s1 in the carrier of I[01] & s2 in the carrier of I[01] ) by A4, A6, BORSUK_1:43; hence s1 <= s2 by A3, A5, A7, FUNCT_2:19; ::_thesis: verum end; hence LE q1,q1,P,p1,p2 by A1, Def3; ::_thesis: verum end; theorem Th10: :: JORDAN5C:10 for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q1 in P implies ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) ) assume that A1: P is_an_arc_of p1,p2 and A2: q1 in P ; ::_thesis: ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) reconsider P = P as non empty Subset of (TOP-REAL 2) by A2; A3: now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P) for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_p1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_q1_&_0_<=_s2_&_s2_<=_1_holds_ s1_<=_s2 A4: 0 in the carrier of I[01] by BORSUK_1:43; let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A5: g is being_homeomorphism and A6: g . 0 = p1 and g . 1 = p2 and A7: g . s1 = p1 and A8: ( 0 <= s1 & s1 <= 1 ) and g . s2 = q1 and A9: 0 <= s2 and s2 <= 1 ; ::_thesis: s1 <= s2 ( s1 in the carrier of I[01] & g is one-to-one ) by A5, A8, BORSUK_1:43, TOPS_2:def_5; hence s1 <= s2 by A6, A7, A9, A4, FUNCT_2:19; ::_thesis: verum end; A10: now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P) for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_q1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_p2_&_0_<=_s2_&_s2_<=_1_holds_ s1_<=_s2 A11: 1 in the carrier of I[01] by BORSUK_1:43; let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A12: g is being_homeomorphism and g . 0 = p1 and A13: g . 1 = p2 and g . s1 = q1 and 0 <= s1 and A14: ( s1 <= 1 & g . s2 = p2 ) and A15: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 ( s2 in the carrier of I[01] & g is one-to-one ) by A12, A15, BORSUK_1:43, TOPS_2:def_5; hence s1 <= s2 by A13, A14, A11, FUNCT_2:19; ::_thesis: verum end; ( p1 in P & p2 in P ) by A1, TOPREAL1:1; hence ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) by A2, A3, A10, Def3; ::_thesis: verum end; theorem :: JORDAN5C:11 for P being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds LE p1,p2,P,p1,p2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds LE p1,p2,P,p1,p2 let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies LE p1,p2,P,p1,p2 ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: LE p1,p2,P,p1,p2 then p2 in P by TOPREAL1:1; hence LE p1,p2,P,p1,p2 by A1, Th10; ::_thesis: verum end; theorem Th12: :: JORDAN5C:12 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds q1 = q2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds q1 = q2 let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 implies q1 = q2 ) assume that A1: P is_an_arc_of p1,p2 and A2: LE q1,q2,P,p1,p2 and A3: LE q2,q1,P,p1,p2 ; ::_thesis: q1 = q2 consider f being Function of I[01],((TOP-REAL 2) | P) such that A4: f is being_homeomorphism and A5: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def_1; A6: dom f = [#] I[01] by A4, TOPS_2:def_5 .= the carrier of I[01] ; A7: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5 .= P by PRE_TOPC:def_5 ; then q2 in rng f by A2, Def3; then consider x being set such that A8: x in dom f and A9: q2 = f . x by FUNCT_1:def_3; q1 in rng f by A2, A7, Def3; then consider y being set such that A10: y in dom f and A11: q1 = f . y by FUNCT_1:def_3; [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1; then consider s3 being Real such that A12: s3 = x and A13: ( 0 <= s3 & s3 <= 1 ) by A6, A8, BORSUK_1:40; [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1; then consider s4 being Real such that A14: s4 = y and A15: ( 0 <= s4 & s4 <= 1 ) by A6, A10, BORSUK_1:40; ( s3 <= s4 & s4 <= s3 ) by A2, A3, A4, A5, A9, A12, A13, A11, A14, A15, Def3; hence q1 = q2 by A9, A12, A11, A14, XXREAL_0:1; ::_thesis: verum end; theorem Th13: :: JORDAN5C:13 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds LE q1,q3,P,p1,p2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds LE q1,q3,P,p1,p2 let p1, p2, q1, q2, q3 be Point of (TOP-REAL 2); ::_thesis: ( LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 implies LE q1,q3,P,p1,p2 ) assume that A1: LE q1,q2,P,p1,p2 and A2: LE q2,q3,P,p1,p2 ; ::_thesis: LE q1,q3,P,p1,p2 A3: q2 in P by A1, Def3; A4: now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P) for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_q1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_q3_&_0_<=_s2_&_s2_<=_1_holds_ s1_<=_s2 A5: [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1; let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A6: g is being_homeomorphism and A7: ( g . 0 = p1 & g . 1 = p2 & g . s1 = q1 ) and 0 <= s1 and A8: ( s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 rng g = [#] ((TOP-REAL 2) | P) by A6, TOPS_2:def_5 .= P by PRE_TOPC:def_5 ; then consider x being set such that A9: x in dom g and A10: q2 = g . x by A3, FUNCT_1:def_3; dom g = [#] I[01] by A6, TOPS_2:def_5 .= the carrier of I[01] ; then consider s3 being Real such that A11: ( s3 = x & 0 <= s3 & s3 <= 1 ) by A9, A5, BORSUK_1:40; ( s1 <= s3 & s3 <= s2 ) by A1, A2, A6, A7, A8, A10, A11, Def3; hence s1 <= s2 by XXREAL_0:2; ::_thesis: verum end; ( q1 in P & q3 in P ) by A1, A2, Def3; hence LE q1,q3,P,p1,p2 by A4, Def3; ::_thesis: verum end; theorem :: JORDAN5C:14 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) implies ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) ) assume that A1: P is_an_arc_of p1,p2 and A2: q1 in P and A3: q2 in P and A4: q1 <> q2 ; ::_thesis: ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) ) reconsider P = P as non empty Subset of (TOP-REAL 2) by A2; ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) ) proof consider f being Function of I[01],((TOP-REAL 2) | P) such that A5: f is being_homeomorphism and A6: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def_1; A7: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def_5 .= P by PRE_TOPC:def_5 ; then consider x being set such that A8: x in dom f and A9: q1 = f . x by A2, FUNCT_1:def_3; consider y being set such that A10: y in dom f and A11: q2 = f . y by A3, A7, FUNCT_1:def_3; dom f = [#] I[01] by A5, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then reconsider s1 = x, s2 = y as Real by A8, A10; A12: 0 <= s1 by A8, BORSUK_1:43; A13: s2 <= 1 by A10, BORSUK_1:43; A14: 0 <= s2 by A10, BORSUK_1:43; A15: s1 <= 1 by A8, BORSUK_1:43; assume A16: ( LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2 ) ; ::_thesis: contradiction percases ( s1 < s2 or s1 = s2 or s1 > s2 ) by XXREAL_0:1; suppose s1 < s2 ; ::_thesis: contradiction hence contradiction by A1, A4, A16, A5, A6, A9, A11, A12, A15, A13, Th8, Th12; ::_thesis: verum end; suppose s1 = s2 ; ::_thesis: contradiction hence contradiction by A4, A9, A11; ::_thesis: verum end; suppose s1 > s2 ; ::_thesis: contradiction hence contradiction by A1, A4, A16, A5, A6, A9, A11, A15, A14, A13, Th8, Th12; ::_thesis: verum end; end; end; hence ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) ) ; ::_thesis: verum end; begin theorem Th15: :: JORDAN5C:15 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) let q be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) ) assume that A1: f is being_S-Seq and A2: (L~ f) /\ Q is closed and A3: q in L~ f and A4: q in Q ; ::_thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) set P = L~ f; A5: (L~ f) /\ Q c= L~ f by XBOOLE_1:17; set q1 = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q); ( L~ f meets Q & L~ f is_an_arc_of f /. 1,f /. (len f) ) by A1, A3, A4, TOPREAL1:25, XBOOLE_0:3; then ( First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | (L~ f)) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ) by A2, A4, Def1; hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A3, A5, Def3; ::_thesis: verum end; theorem Th16: :: JORDAN5C:16 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) let q be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) ) set P = L~ f; assume that A1: f is being_S-Seq and A2: (L~ f) /\ Q is closed and A3: q in L~ f and A4: q in Q ; ::_thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) set q1 = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q); A5: (L~ f) /\ Q c= L~ f by XBOOLE_1:17; ( L~ f meets Q & L~ f is_an_arc_of f /. 1,f /. (len f) ) by A1, A3, A4, TOPREAL1:25, XBOOLE_0:3; then ( Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | (L~ f)) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ) by A2, A4, Def2; hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A3, A5, Def3; ::_thesis: verum end; theorem Th17: :: JORDAN5C:17 for q1, q2, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 holds LE q1,q2,p1,p2 proof let q1, q2, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 implies LE q1,q2,p1,p2 ) set P = LSeg (p1,p2); assume p1 <> p2 ; ::_thesis: ( not LE q1,q2, LSeg (p1,p2),p1,p2 or LE q1,q2,p1,p2 ) then consider f being Function of I[01],((TOP-REAL 2) | (LSeg (p1,p2))) such that A1: for x being Real st x in [.0,1.] holds f . x = ((1 - x) * p1) + (x * p2) and A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by JORDAN5A:3; assume A3: LE q1,q2, LSeg (p1,p2),p1,p2 ; ::_thesis: LE q1,q2,p1,p2 hence ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) ) by Def3; :: according to JORDAN3:def_5 ::_thesis: for b1, b2 being Element of REAL holds ( not 0 <= b1 or not b1 <= 1 or not q1 = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not q2 = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 ) let r1, r2 be Real; ::_thesis: ( not 0 <= r1 or not r1 <= 1 or not q1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not q2 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 ) assume that A4: 0 <= r1 and A5: r1 <= 1 and A6: q1 = ((1 - r1) * p1) + (r1 * p2) and A7: ( 0 <= r2 & r2 <= 1 ) and A8: q2 = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: r1 <= r2 r2 in [.0,1.] by A7, BORSUK_1:40, BORSUK_1:43; then A9: q2 = f . r2 by A8, A1; r1 in [.0,1.] by A4, A5, BORSUK_1:40, BORSUK_1:43; then q1 = f . r1 by A6, A1; hence r1 <= r2 by A3, A5, A7, A2, A9, Def3; ::_thesis: verum end; theorem :: JORDAN5C:18 for P, Q being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) proof let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed implies ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) ) assume that A1: P is_an_arc_of p1,p2 and A2: P /\ Q <> {} and A3: P /\ Q is closed ; :: according to XBOOLE_0:def_7 ::_thesis: ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) reconsider P = P as non empty Subset of (TOP-REAL 2) by A2; A4: P meets Q by A2, XBOOLE_0:def_7; A5: P is_an_arc_of p2,p1 by A1, JORDAN5B:14; A6: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q proof set Ex = L[01] (((0,1) (#)),((#) (0,1))); let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not f . t in Q let s2 be Real; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds not f . t in Q ) assume that A7: f is being_homeomorphism and A8: f . 0 = p1 and A9: f . 1 = p2 and A10: f . s2 = Last_Point (P,p2,p1,Q) and A11: 0 <= s2 and A12: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds not f . t in Q set s21 = 1 - s2; set g = f * (L[01] (((0,1) (#)),((#) (0,1)))); A13: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18; dom f = [#] I[01] by A7, TOPS_2:def_5; then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A13, TOPMETR:20, TOPS_2:def_5; then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27; then A14: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A13, TOPMETR:20, TOPS_2:def_5; reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20; A15: ( 1 - 1 <= 1 - s2 & 1 - s2 <= 1 - 0 ) by A11, A12, XREAL_1:13; then A16: 1 - s2 in dom g by A14, BORSUK_1:43; (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9; then A17: g . 0 = p2 by A9, A14, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5; (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9; then A18: g . 1 = p1 by A8, A14, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5; let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not f . t in Q ) assume that A19: 0 <= t and A20: t < s2 ; ::_thesis: not f . t in Q A21: 1 - t <= 1 - 0 by A19, XREAL_1:13; t <= 1 by A12, A20, XXREAL_0:2; then A22: 1 - 1 <= 1 - t by XREAL_1:13; then reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A15, A21, BORSUK_1:43, TOPMETR:20; A23: 1 - t in dom g by A14, A22, A21, BORSUK_1:43; (L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3 .= s2 ; then A24: g . (1 - s2) = f . s2 by A16, FUNCT_1:12; (L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3 .= t ; then A25: g . t9 = f . t by A23, FUNCT_1:12; A26: 1 - s2 < 1 - t by A20, XREAL_1:15; g is being_homeomorphism by A7, A13, TOPMETR:20, TOPS_2:57; hence not f . t in Q by A3, A5, A4, A10, A17, A18, A15, A21, A24, A25, A26, Def2; ::_thesis: verum end; A27: for g being Function of I[01],((TOP-REAL 2) | P) for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q proof set Ex = L[01] (((0,1) (#)),((#) (0,1))); let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not f . t in Q let s2 be Real; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds not f . t in Q ) assume that A28: f is being_homeomorphism and A29: f . 0 = p1 and A30: f . 1 = p2 and A31: f . s2 = First_Point (P,p2,p1,Q) and A32: 0 <= s2 and A33: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds not f . t in Q set g = f * (L[01] (((0,1) (#)),((#) (0,1)))); A34: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18; dom f = [#] I[01] by A28, TOPS_2:def_5; then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A34, TOPMETR:20, TOPS_2:def_5; then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27; then A35: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A34, TOPMETR:20, TOPS_2:def_5; let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not f . t in Q ) assume that A36: 1 >= t and A37: t > s2 ; ::_thesis: not f . t in Q A38: 1 - s2 > 1 - t by A37, XREAL_1:15; set s21 = 1 - s2; A39: 1 - s2 <= 1 - 0 by A32, XREAL_1:13; reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20; A40: 1 - 1 <= 1 - t by A36, XREAL_1:13; A41: 1 - t <= 1 - 0 by A32, A37, XREAL_1:13; then A42: 1 - t in dom g by A35, A40, BORSUK_1:43; A43: 1 - 1 <= 1 - s2 by A33, XREAL_1:13; then A44: 1 - s2 in dom g by A35, A39, BORSUK_1:43; reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A43, A39, A40, A41, BORSUK_1:43, TOPMETR:20; (L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3 .= s2 ; then A45: g . (1 - s2) = f . s2 by A44, FUNCT_1:12; (L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3 .= t ; then A46: g . t9 = f . t by A42, FUNCT_1:12; (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9; then A47: g . 0 = p2 by A30, A35, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5; (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9; then A48: g . 1 = p1 by A29, A35, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5; g is being_homeomorphism by A28, A34, TOPMETR:20, TOPS_2:57; hence not f . t in Q by A3, A5, A4, A31, A47, A48, A39, A40, A45, A46, A38, Def1; ::_thesis: verum end; ( Last_Point (P,p2,p1,Q) in P /\ Q & First_Point (P,p2,p1,Q) in P /\ Q ) by A3, A5, A4, Def1, Def2; hence ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) by A1, A3, A4, A6, A27, Def1, Def2; ::_thesis: verum end; theorem Th19: :: JORDAN5C:19 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) let Q be Subset of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) let i be Element of NAT ; ::_thesis: ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ) assume that A1: L~ f meets Q and A2: Q is closed and A3: f is being_S-Seq and A4: ( 1 <= i & i + 1 <= len f ) and A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) ; ::_thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) len f >= 2 by A3, TOPREAL1:def_8; then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of the carrier of (TOP-REAL 2) by A5, TOPREAL1:23; A6: P is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25; set FPO = First_Point (R,(f /. i),(f /. (i + 1)),Q); set FPG = First_Point (P,(f /. 1),(f /. (len f)),Q); A7: (L~ f) /\ Q is closed by A2, TOPS_1:8; then First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A6, Def1; then A8: First_Point (P,(f /. 1),(f /. (len f)),Q) in Q by XBOOLE_0:def_4; A9: i + 1 in dom f by A4, SEQ_4:134; A10: ( f is one-to-one & i in dom f ) by A3, A4, SEQ_4:134, TOPREAL1:def_8; A11: f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A10, A9, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) proof First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A7, A6, Def1; then A12: First_Point (P,(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def_4; consider F being Function of I[01],((TOP-REAL 2) | P) such that A13: F is being_homeomorphism and A14: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) by A6, TOPREAL1:def_1; rng F = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def_5 .= L~ f by PRE_TOPC:def_5 ; then consider s21 being set such that A15: s21 in dom F and A16: F . s21 = First_Point (P,(f /. 1),(f /. (len f)),Q) by A12, FUNCT_1:def_3; A17: dom F = [#] I[01] by A13, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then reconsider s21 = s21 as Real by A15; A18: s21 <= 1 by A15, BORSUK_1:43; A19: for g being Function of I[01],((TOP-REAL 2) | R) for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q proof consider ppi, pi1 being Real such that A20: ppi < pi1 and A21: 0 <= ppi and ppi <= 1 and 0 <= pi1 and A22: pi1 <= 1 and A23: LSeg (f,i) = F .: [.ppi,pi1.] and A24: F . ppi = f /. i and A25: F . pi1 = f /. (i + 1) by A3, A4, A13, A14, JORDAN5B:7; A26: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20; then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A21, A22, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34; consider hh being Function of (I[01] | Poz),((TOP-REAL 2) | R) such that A27: hh = F | Poz and A28: hh is being_homeomorphism by A3, A4, A13, A14, A23, JORDAN5B:8; A29: hh = F * (id Poz) by A27, RELAT_1:65; A30: [.ppi,pi1.] c= [.0,1.] by A21, A22, XXREAL_1:34; reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR:20, TREAL_1:3; Poz = [#] A by A20, TOPMETR:18; then A31: I[01] | Poz = A by PRE_TOPC:def_5; hh " is being_homeomorphism by A28, TOPS_2:56; then A32: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def_5; pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20; then pi1 in [.ppi,pi1.] by RCOMP_1:def_1; then pi1 in (dom F) /\ Poz by A17, A30, XBOOLE_0:def_4; then A33: pi1 in dom hh by A27, RELAT_1:61; then A34: hh . pi1 = f /. (i + 1) by A25, A27, FUNCT_1:47; the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P) .= P by PRE_TOPC:def_5 ; then reconsider SEG = LSeg (f,i) as non empty Subset of the carrier of ((TOP-REAL 2) | P) by A5, TOPREAL3:19; A35: the carrier of (((TOP-REAL 2) | P) | SEG) = [#] (((TOP-REAL 2) | P) | SEG) .= SEG by PRE_TOPC:def_5 ; reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ; let g be Function of I[01],((TOP-REAL 2) | R); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 0 <= t & t < s2 holds not g . t in Q let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds not g . t in Q ) assume that A36: g is being_homeomorphism and A37: g . 0 = f /. i and A38: g . 1 = f /. (i + 1) and A39: g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) and A40: 0 <= s2 and A41: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds not g . t in Q A42: ( g is continuous & g is one-to-one ) by A36, TOPS_2:def_5; reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | P) ; A43: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2; ppi in [.ppi,pi1.] by A26, RCOMP_1:def_1; then ppi in (dom F) /\ Poz by A17, A30, XBOOLE_0:def_4; then A44: ppi in dom hh by A27, RELAT_1:61; then A45: hh . ppi = f /. i by A24, A27, FUNCT_1:47; A46: dom hh = [#] (I[01] | Poz) by A28, TOPS_2:def_5; then A47: dom hh = Poz by PRE_TOPC:def_5; A48: rng hh = hh .: (dom hh) by A46, RELSET_1:22 .= [#] (((TOP-REAL 2) | P) | SEG) by A23, A35, A27, A47, RELAT_1:129 ; let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in Q ) assume that A49: 0 <= t and A50: t < s2 ; ::_thesis: not g . t in Q A51: t < 1 by A41, A50, XXREAL_0:2; then reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A40, A41, A49, BORSUK_1:43, TOPMETR:20; A52: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def_5; set H = (hh ") * g; A53: rng g = [#] ((TOP-REAL 2) | SE) by A36, TOPS_2:def_5; set ss = ((hh ") * g) . t; A54: hh is one-to-one by A28, TOPS_2:def_5; A55: hh is one-to-one by A28, TOPS_2:def_5; then A56: dom (hh ") = [#] (((TOP-REAL 2) | P) | SEG) by A43, A48, TOPS_2:49; then A57: rng ((hh ") * g) = rng (hh ") by A53, RELAT_1:28; A58: rng (hh ") = [#] (I[01] | Poz) by A43, A55, A48, TOPS_2:49 .= Poz by PRE_TOPC:def_5 ; then rng ((hh ") * g) = Poz by A53, A56, RELAT_1:28; then A59: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18; hh is onto by A43, A48, FUNCT_2:def_3; then A60: hh " = hh " by A55, TOPS_2:def_4; A61: dom g = [#] I[01] by A36, TOPS_2:def_5 .= the carrier of I[01] ; then A62: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A43, A53, A56, RELAT_1:27, TOPMETR:20; A63: t in dom g by A61, A49, A51, BORSUK_1:43; then g . t in [#] ((TOP-REAL 2) | SE) by A53, FUNCT_1:def_3; then A64: g . t in SEG by PRE_TOPC:def_5; then consider x being set such that A65: x in dom F and A66: x in Poz and A67: g . t = F . x by A23, FUNCT_1:def_6; A68: F is one-to-one by A52; then A69: (F ") . (g . t) in Poz by A65, A66, A67, FUNCT_1:32; F is onto by A52, FUNCT_2:def_3; then A70: F " = F " by A52, TOPS_2:def_4; x = (F ") . (g . t) by A68, A65, A67, FUNCT_1:32; then (F ") . (g . t) in Poz by A66, A70; then A71: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17; g . t in the carrier of ((TOP-REAL 2) | P) by A64; then A72: g . t in dom (F ") by A52, TOPS_2:49; t in dom ((hh ") * g) by A43, A53, A63, A56, RELAT_1:27; then A73: F . (((hh ") * g) . t) = (((hh ") * g) * F) . t by FUNCT_1:13 .= (g * ((hh ") * F)) . t by RELAT_1:36 .= (F * (hh ")) . (g . t) by A63, FUNCT_1:13 .= (F * ((F ") * ((id Poz) "))) . (g . t) by A68, A29, A60, FUNCT_1:44 .= (((F ") * ((id Poz) ")) * F) . (g . t) by A70 .= ((F ") * (((id Poz) ") * F)) . (g . t) by RELAT_1:36 .= ((F ") * (F * (id Poz))) . (g . t) by FUNCT_1:45 .= (F * (id Poz)) . ((F ") . (g . t)) by A72, FUNCT_1:13 .= F . ((id Poz) . ((F ") . (g . t))) by A71, FUNCT_1:13 .= F . ((F ") . (g . t)) by A69, A70, FUNCT_1:17 .= g . t by A52, A64, FUNCT_1:35 ; 1 in dom g by A61, BORSUK_1:43; then A74: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A38, FUNCT_1:13 .= pi1 by A54, A33, A34, A60, FUNCT_1:32 ; 0 in dom g by A61, BORSUK_1:43; then A75: ((hh ") * g) . 0 = (hh ") . (f /. i) by A37, FUNCT_1:13 .= ppi by A54, A44, A45, A60, FUNCT_1:32 ; dom ((hh ") * g) = dom g by A43, A53, A56, RELAT_1:27; then ((hh ") * g) . t in Poz by A58, A63, A57, FUNCT_1:def_3; then ((hh ") * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) } by RCOMP_1:def_1; then consider ss9 being Real such that A76: ss9 = ((hh ") * g) . t and A77: ppi <= ss9 and ss9 <= pi1 ; reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A62, A59, FUNCT_2:2; A78: ss9 = H . w2 by A76; ex z being set st ( z in dom F & z in Poz & F . s21 = F . z ) by A5, A16, A23, FUNCT_1:def_6; then A79: s21 in Poz by A15, A68, FUNCT_1:def_4; then hh . s21 = g . s2 by A16, A39, A27, FUNCT_1:49; then s21 = (hh ") . (g . s2) by A55, A47, A79, FUNCT_1:32; then A80: s21 = (hh ") . (g . s2) by A60; s2 in dom g by A40, A41, A61, BORSUK_1:43; then s21 = H . w1 by A80, FUNCT_1:13; then ss9 < s21 by A20, A50, A75, A74, A42, A32, A31, A78, JORDAN5A:15, TOPMETR:20; hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1; ::_thesis: verum end; A81: (LSeg (f,i)) /\ Q is closed by A2, TOPS_1:8; (LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def_4; then A82: LSeg (f,i) meets Q by XBOOLE_0:def_7; LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3; then A83: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9; First_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def_4; hence First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) by A82, A81, A83, A19, Def1; ::_thesis: verum end; hence First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ; ::_thesis: verum end; theorem Th20: :: JORDAN5C:20 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) let Q be Subset of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) let i be Element of NAT ; ::_thesis: ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ) assume that A1: L~ f meets Q and A2: Q is closed and A3: f is being_S-Seq and A4: ( 1 <= i & i + 1 <= len f ) and A5: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) ; ::_thesis: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) len f >= 2 by A3, TOPREAL1:def_8; then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5, TOPREAL1:23; A6: P is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25; set FPO = Last_Point (R,(f /. i),(f /. (i + 1)),Q); set FPG = Last_Point (P,(f /. 1),(f /. (len f)),Q); A7: (L~ f) /\ Q is closed by A2, TOPS_1:8; then Last_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A6, Def2; then A8: Last_Point (P,(f /. 1),(f /. (len f)),Q) in Q by XBOOLE_0:def_4; A9: i + 1 in dom f by A4, SEQ_4:134; A10: ( f is one-to-one & i in dom f ) by A3, A4, SEQ_4:134, TOPREAL1:def_8; A11: f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A10, A9, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) proof Last_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A7, A6, Def2; then A12: Last_Point (P,(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def_4; consider F being Function of I[01],((TOP-REAL 2) | P) such that A13: F is being_homeomorphism and A14: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) by A6, TOPREAL1:def_1; rng F = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def_5 .= L~ f by PRE_TOPC:def_5 ; then consider s21 being set such that A15: s21 in dom F and A16: F . s21 = Last_Point (P,(f /. 1),(f /. (len f)),Q) by A12, FUNCT_1:def_3; A17: dom F = [#] I[01] by A13, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then reconsider s21 = s21 as Real by A15; A18: ( 0 <= s21 & s21 <= 1 ) by A15, BORSUK_1:43; A19: for g being Function of I[01],((TOP-REAL 2) | R) for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q proof consider ppi, pi1 being Real such that A20: ppi < pi1 and A21: 0 <= ppi and ppi <= 1 and 0 <= pi1 and A22: pi1 <= 1 and A23: LSeg (f,i) = F .: [.ppi,pi1.] and A24: F . ppi = f /. i and A25: F . pi1 = f /. (i + 1) by A3, A4, A13, A14, JORDAN5B:7; A26: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20; then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A21, A22, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34; A27: [.ppi,pi1.] c= [.0,1.] by A21, A22, XXREAL_1:34; reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR:20, TREAL_1:3; A28: Poz = [#] A by A20, TOPMETR:18; then A29: I[01] | Poz = A by PRE_TOPC:def_5; Closed-Interval-TSpace (ppi,pi1) is compact by A20, HEINE:4; then [#] (Closed-Interval-TSpace (ppi,pi1)) is compact by COMPTS_1:1; then for P being Subset of A st P = Poz holds P is compact by A20, TOPMETR:18; then Poz is compact by A28, COMPTS_1:2; then A30: I[01] | Poz is compact by COMPTS_1:3; reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A6; let g be Function of I[01],((TOP-REAL 2) | R); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds for t being Real st 1 >= t & t > s2 holds not g . t in Q let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds not g . t in Q ) assume that A31: g is being_homeomorphism and A32: g . 0 = f /. i and A33: g . 1 = f /. (i + 1) and A34: g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) and A35: 0 <= s2 and A36: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds not g . t in Q the carrier of ((TOP-REAL 2) | Lf) = [#] ((TOP-REAL 2) | Lf) .= Lf by PRE_TOPC:def_5 ; then reconsider SEG = LSeg (f,i) as non empty Subset of ((TOP-REAL 2) | Lf) by A5, TOPREAL3:19; reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ; A37: rng g = [#] ((TOP-REAL 2) | SE) by A31, TOPS_2:def_5; set gg = F | Poz; A38: the carrier of (I[01] | Poz) = [#] (I[01] | Poz) .= Poz by PRE_TOPC:def_5 ; then reconsider gg = F | Poz as Function of (I[01] | Poz),((TOP-REAL 2) | P) by FUNCT_2:32; let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in Q ) assume that A39: 1 >= t and A40: t > s2 ; ::_thesis: not g . t in Q A41: rng gg c= SEG proof let ii be set ; :: according to TARSKI:def_3 ::_thesis: ( not ii in rng gg or ii in SEG ) assume ii in rng gg ; ::_thesis: ii in SEG then consider j being set such that A42: j in dom gg and A43: ii = gg . j by FUNCT_1:def_3; j in (dom F) /\ Poz by A42, RELAT_1:61; then j in dom F by XBOOLE_0:def_4; then F . j in LSeg (f,i) by A23, A38, A42, FUNCT_1:def_6; hence ii in SEG by A38, A42, A43, FUNCT_1:49; ::_thesis: verum end; A44: the carrier of (((TOP-REAL 2) | Lf) | SEG) = [#] (((TOP-REAL 2) | Lf) | SEG) .= SEG by PRE_TOPC:def_5 ; reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | Lf) ; reconsider hh9 = gg as Function of (I[01] | Poz),(((TOP-REAL 2) | Lf) | SEG) by A44, A41, FUNCT_2:6; reconsider hh = hh9 as Function of (I[01] | Poz),((TOP-REAL 2) | SE) by GOBOARD9:2; A45: dom hh = [#] (I[01] | Poz) by FUNCT_2:def_1; then A46: dom hh = Poz by PRE_TOPC:def_5; A47: rng hh = hh .: (dom hh) by A45, RELSET_1:22 .= [#] (((TOP-REAL 2) | Lf) | SEG) by A23, A44, A46, RELAT_1:129 ; A48: F is one-to-one by A13, TOPS_2:def_5; then A49: hh is one-to-one by FUNCT_1:52; set H = (hh ") * g; A50: ((TOP-REAL 2) | Lf) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2; A51: hh9 is one-to-one by A48, FUNCT_1:52; then A52: dom (hh ") = [#] (((TOP-REAL 2) | Lf) | SEG) by A50, A47, TOPS_2:49; then A53: rng ((hh ") * g) = rng (hh ") by A37, RELAT_1:28; A54: dom g = [#] I[01] by A31, TOPS_2:def_5 .= the carrier of I[01] ; then A55: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A50, A37, A52, RELAT_1:27, TOPMETR:20; A56: t in dom g by A35, A54, A39, A40, BORSUK_1:43; then g . t in [#] ((TOP-REAL 2) | SE) by A37, FUNCT_1:def_3; then A57: g . t in SEG by PRE_TOPC:def_5; then consider x being set such that A58: x in dom F and A59: x in Poz and A60: g . t = F . x by A23, FUNCT_1:def_6; hh is onto by A50, A47, FUNCT_2:def_3; then A61: hh " = hh " by A51, TOPS_2:def_4; A62: (F ") . (g . t) in Poz by A48, A58, A59, A60, FUNCT_1:32; ex z being set st ( z in dom F & z in Poz & F . s21 = F . z ) by A5, A16, A23, FUNCT_1:def_6; then A63: s21 in Poz by A15, A48, FUNCT_1:def_4; then hh . s21 = g . s2 by A16, A34, FUNCT_1:49; then s21 = (hh ") . (g . s2) by A51, A46, A63, FUNCT_1:32; then A64: s21 = (hh ") . (g . s2) by A61; A65: ( g is continuous & g is one-to-one ) by A31, TOPS_2:def_5; A66: (TOP-REAL 2) | SE is T_2 by TOPMETR:2; reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A35, A36, A39, A40, BORSUK_1:43, TOPMETR:20; A67: hh = F * (id Poz) by RELAT_1:65; set ss = ((hh ") * g) . t; A68: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def_5; A69: rng (hh ") = [#] (I[01] | Poz) by A50, A51, A47, TOPS_2:49 .= Poz by PRE_TOPC:def_5 ; then rng ((hh ") * g) = Poz by A37, A52, RELAT_1:28; then A70: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18; dom ((hh ") * g) = dom g by A50, A37, A52, RELAT_1:27; then ((hh ") * g) . t in Poz by A69, A56, A53, FUNCT_1:def_3; then ((hh ") * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) } by RCOMP_1:def_1; then consider ss9 being Real such that A71: ss9 = ((hh ") * g) . t and ppi <= ss9 and A72: ss9 <= pi1 ; F is onto by A68, FUNCT_2:def_3; then A73: F " = F " by A68, TOPS_2:def_4; A74: 1 >= ss9 by A22, A72, XXREAL_0:2; x = (F ") . (g . t) by A48, A58, A60, FUNCT_1:32; then (F ") . (g . t) in Poz by A59, A73; then A75: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17; g . t in the carrier of ((TOP-REAL 2) | Lf) by A57; then A76: g . t in dom (F ") by A68, TOPS_2:49; t in dom ((hh ") * g) by A50, A37, A56, A52, RELAT_1:27; then A77: F . (((hh ") * g) . t) = (((hh ") * g) * F) . t by FUNCT_1:13 .= (g * ((hh ") * F)) . t by RELAT_1:36 .= (F * (hh ")) . (g . t) by A56, FUNCT_1:13 .= (F * (hh ")) . (g . t) by A61 .= (F * ((F ") * ((id Poz) "))) . (g . t) by A48, A67, FUNCT_1:44 .= (((F ") * ((id Poz) ")) * F) . (g . t) by A73 .= ((F ") * (((id Poz) ") * F)) . (g . t) by RELAT_1:36 .= ((F ") * (F * (id Poz))) . (g . t) by FUNCT_1:45 .= (F * (id Poz)) . ((F ") . (g . t)) by A76, FUNCT_1:13 .= F . ((id Poz) . ((F ") . (g . t))) by A75, FUNCT_1:13 .= F . ((id Poz) . ((F ") . (g . t))) by A73 .= F . ((F ") . (g . t)) by A62, FUNCT_1:17 .= g . t by A68, A57, FUNCT_1:35 ; pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20; then pi1 in [.ppi,pi1.] by RCOMP_1:def_1; then pi1 in (dom F) /\ Poz by A17, A27, XBOOLE_0:def_4; then A78: pi1 in dom hh by RELAT_1:61; then A79: hh . pi1 = f /. (i + 1) by A25, FUNCT_1:47; F is continuous by A13, TOPS_2:def_5; then gg is continuous by TOPMETR:7; then hh is being_homeomorphism by A50, A51, A45, A47, A30, A66, COMPTS_1:17, TOPMETR:6; then hh " is being_homeomorphism by TOPS_2:56; then A80: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def_5; ppi in [.ppi,pi1.] by A26, RCOMP_1:def_1; then ppi in (dom F) /\ Poz by A17, A27, XBOOLE_0:def_4; then A81: ppi in dom hh by RELAT_1:61; then A82: hh . ppi = f /. i by A24, FUNCT_1:47; 1 in dom g by A54, BORSUK_1:43; then A83: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A33, FUNCT_1:13 .= pi1 by A49, A78, A79, A61, FUNCT_1:32 ; 0 in dom g by A54, BORSUK_1:43; then A84: ((hh ") * g) . 0 = (hh ") . (f /. i) by A32, FUNCT_1:13 .= ppi by A49, A81, A82, A61, FUNCT_1:32 ; reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A55, A70, FUNCT_2:2; s2 in dom g by A35, A36, A54, BORSUK_1:43; then A85: s21 = H . w1 by A64, FUNCT_1:13; ss9 = H . w2 by A71; then ss9 > s21 by A20, A40, A84, A83, A65, A80, A29, A85, JORDAN5A:15, TOPMETR:20; hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A71, A74, A77, Def2; ::_thesis: verum end; A86: (LSeg (f,i)) /\ Q is closed by A2, TOPS_1:8; (LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def_4; then A87: LSeg (f,i) meets Q by XBOOLE_0:def_7; LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3; then A88: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9; Last_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def_4; hence Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A87, A86, A88, A19, Def2; ::_thesis: verum end; hence Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ; ::_thesis: verum end; theorem :: JORDAN5C:21 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i ) assume that A1: ( 1 <= i & i + 1 <= len f ) and A2: f is being_S-Seq and A3: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; ::_thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A3; Q = LSeg ((f /. i),(f /. (i + 1))) by A1, TOPREAL1:def_3; then Q c= L~ f by A1, SPPOL_2:16; then L~ f meets Q by A3, XBOOLE_0:3; then A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th19; ( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15; hence First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i by A4, Th7; ::_thesis: verum end; theorem :: JORDAN5C:22 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) ) assume that A1: ( 1 <= i & i + 1 <= len f ) and A2: f is being_S-Seq and A3: Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; ::_thesis: Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A3; Q = LSeg ((f /. i),(f /. (i + 1))) by A1, TOPREAL1:def_3; then Q c= L~ f by A1, SPPOL_2:16; then L~ f meets Q by A3, XBOOLE_0:3; then A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th20; ( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15; hence Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) by A4, Th7; ::_thesis: verum end; theorem Th23: :: JORDAN5C:23 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f holds LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f holds LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f implies LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) ) assume that A1: f is being_S-Seq and A2: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) set p1 = f /. 1; set p2 = f /. (len f); set q1 = f /. i; set q2 = f /. (i + 1); A3: len f >= 2 by A1, TOPREAL1:def_8; then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23; i + 1 in dom f by A2, SEQ_4:134; then A4: f /. (i + 1) in P by A3, GOBOARD1:1; A5: for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds s1 <= s2 proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A6: g is being_homeomorphism and A7: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and A8: g . s1 = f /. i and A9: ( 0 <= s1 & s1 <= 1 ) and A10: g . s2 = f /. (i + 1) and A11: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 A12: dom g = [#] I[01] by A6, TOPS_2:def_5 .= the carrier of I[01] ; then A13: s1 in dom g by A9, BORSUK_1:43; A14: s2 in dom g by A11, A12, BORSUK_1:43; A15: g is one-to-one by A6, TOPS_2:def_5; consider r1, r2 being Real such that A16: r1 < r2 and A17: 0 <= r1 and A18: r1 <= 1 and 0 <= r2 and A19: r2 <= 1 and LSeg (f,i) = g .: [.r1,r2.] and A20: g . r1 = f /. i and A21: g . r2 = f /. (i + 1) by A1, A2, A6, A7, JORDAN5B:7; A22: r2 in dom g by A16, A17, A19, A12, BORSUK_1:43; r1 in dom g by A17, A18, A12, BORSUK_1:43; then s1 = r1 by A8, A20, A13, A15, FUNCT_1:def_4; hence s1 <= s2 by A10, A16, A21, A22, A14, A15, FUNCT_1:def_4; ::_thesis: verum end; i in dom f by A2, SEQ_4:134; then f /. i in P by A3, GOBOARD1:1; hence LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5, Def3; ::_thesis: verum end; theorem Th24: :: JORDAN5C:24 for f being FinSequence of (TOP-REAL 2) for i, j being Element of NAT st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) let i, j be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i <= j & j <= len f implies LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) ) assume that A1: f is being_S-Seq and A2: 1 <= i and A3: i <= j and A4: j <= len f ; ::_thesis: LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) consider k being Nat such that A5: i + k = j by A3, NAT_1:10; A6: len f >= 2 by A1, TOPREAL1:def_8; then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23; defpred S1[ Element of NAT ] means ( 1 <= i & i + $1 <= len f implies LE f /. i,f /. (i + $1),P,f /. 1,f /. (len f) ); A7: for l being Element of NAT st S1[l] holds S1[l + 1] proof let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A8: S1[l] ; ::_thesis: S1[l + 1] A9: i + l <= (i + l) + 1 by NAT_1:11; assume that A10: 1 <= i and A11: i + (l + 1) <= len f ; ::_thesis: LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f) A12: (i + l) + 1 <= len f by A11; i <= i + l by NAT_1:11; then 1 <= i + l by A10, XXREAL_0:2; then LE f /. (i + l),f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A1, A12, Th23; hence LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A8, A10, A11, A9, Th13, XXREAL_0:2; ::_thesis: verum end; A13: S1[ 0 ] proof assume ( 1 <= i & i + 0 <= len f ) ; ::_thesis: LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f) then i in dom f by FINSEQ_3:25; hence LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f) by A6, Th9, GOBOARD1:1; ::_thesis: verum end; A14: for l being Element of NAT holds S1[l] from NAT_1:sch_1(A13, A7); k in NAT by ORDINAL1:def_12; hence LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) by A2, A4, A5, A14; ::_thesis: verum end; Lm1: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) let i be Element of NAT ; ::_thesis: ( LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) ) assume that A1: LSeg (f,i) meets Q and A2: f is being_S-Seq and A3: Q is closed and A4: ( 1 <= i & i + 1 <= len f ) and A5: q in LSeg (f,i) and A6: q in Q ; ::_thesis: LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) reconsider P = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5; set q1 = First_Point (P,(f /. i),(f /. (i + 1)),Q); set p1 = f /. i; set p2 = f /. (i + 1); A7: P /\ Q c= P by XBOOLE_1:17; A8: i + 1 in dom f by A4, SEQ_4:134; A9: ( f is one-to-one & i in dom f ) by A2, A4, SEQ_4:134, TOPREAL1:def_8; A10: f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A9, A8, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; A11: P /\ Q is closed by A3, TOPS_1:8; P is_an_arc_of f /. i,f /. (i + 1) by A2, A4, JORDAN5B:15; then ( First_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = First_Point (P,(f /. i),(f /. (i + 1)),Q) & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ) by A1, A6, A11, Def1; then A12: LE First_Point (P,(f /. i),(f /. (i + 1)),Q),q,P,f /. i,f /. (i + 1) by A5, A7, Def3; LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3; hence LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) by A10, A12, Th17; ::_thesis: verum end; Lm2: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) let i be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) assume that A1: L~ f meets Q and A2: f is being_S-Seq and A3: Q is closed and A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and A5: ( 1 <= i & i + 1 <= len f ) and A6: ( q in LSeg (f,i) & q in Q ) ; ::_thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) len f >= 2 by A2, TOPREAL1:def_8; then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:23; (LSeg (f,i)) /\ Q <> {} by A6, XBOOLE_0:def_4; then A7: LSeg (f,i) meets Q by XBOOLE_0:def_7; First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th19; hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm1; ::_thesis: verum end; Lm3: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) let i be Element of NAT ; ::_thesis: ( LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) ) assume that A1: LSeg (f,i) meets Q and A2: f is being_S-Seq and A3: Q is closed and A4: ( 1 <= i & i + 1 <= len f ) and A5: q in LSeg (f,i) and A6: q in Q ; ::_thesis: LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) reconsider P = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5; set q1 = Last_Point (P,(f /. i),(f /. (i + 1)),Q); set p1 = f /. i; set p2 = f /. (i + 1); A7: P /\ Q c= P by XBOOLE_1:17; A8: i + 1 in dom f by A4, SEQ_4:134; A9: ( f is one-to-one & i in dom f ) by A2, A4, SEQ_4:134, TOPREAL1:def_8; A10: f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A9, A8, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; A11: P /\ Q is closed by A3, TOPS_1:8; P is_an_arc_of f /. i,f /. (i + 1) by A2, A4, JORDAN5B:15; then ( Last_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = Last_Point (P,(f /. i),(f /. (i + 1)),Q) & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ) by A1, A6, A11, Def2; then A12: LE q, Last_Point (P,(f /. i),(f /. (i + 1)),Q),P,f /. i,f /. (i + 1) by A5, A7, Def3; LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3; hence LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) by A10, A12, Th17; ::_thesis: verum end; Lm4: for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) let i be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) assume that A1: L~ f meets Q and A2: f is being_S-Seq and A3: Q is closed and A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and A5: ( 1 <= i & i + 1 <= len f ) and A6: ( q in LSeg (f,i) & q in Q ) ; ::_thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) len f >= 2 by A2, TOPREAL1:def_8; then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:23; (LSeg (f,i)) /\ Q <> {} by A6, XBOOLE_0:def_4; then A7: LSeg (f,i) meets Q by XBOOLE_0:def_7; Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th20; hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm3; ::_thesis: verum end; theorem Th25: :: JORDAN5C:25 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds LE f /. i,q, L~ f,f /. 1,f /. (len f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds LE f /. i,q, L~ f,f /. 1,f /. (len f) let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds LE f /. i,q, L~ f,f /. 1,f /. (len f) let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) implies LE f /. i,q, L~ f,f /. 1,f /. (len f) ) assume that A1: f is being_S-Seq and A2: ( 1 <= i & i + 1 <= len f ) and A3: q in LSeg (f,i) ; ::_thesis: LE f /. i,q, L~ f,f /. 1,f /. (len f) set p1 = f /. 1; set p2 = f /. (len f); set q1 = f /. i; A4: 2 <= len f by A1, TOPREAL1:def_8; then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23; i in dom f by A2, SEQ_4:134; then A5: f /. i in P by A4, GOBOARD1:1; A6: for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds s1 <= s2 proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A7: g is being_homeomorphism and A8: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and A9: g . s1 = f /. i and A10: ( 0 <= s1 & s1 <= 1 ) and A11: g . s2 = q and A12: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 A13: dom g = [#] I[01] by A7, TOPS_2:def_5 .= the carrier of I[01] ; then A14: s1 in dom g by A10, BORSUK_1:43; consider r1, r2 being Real such that r1 < r2 and A15: ( 0 <= r1 & r1 <= 1 ) and 0 <= r2 and r2 <= 1 and A16: LSeg (f,i) = g .: [.r1,r2.] and A17: g . r1 = f /. i and g . r2 = f /. (i + 1) by A1, A2, A7, A8, JORDAN5B:7; consider r39 being set such that A18: r39 in dom g and A19: r39 in [.r1,r2.] and A20: g . r39 = q by A3, A16, FUNCT_1:def_6; r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by A19, RCOMP_1:def_1; then consider r3 being Real such that A21: r3 = r39 and A22: r1 <= r3 and r3 <= r2 ; A23: g is one-to-one by A7, TOPS_2:def_5; A24: r1 in dom g by A15, A13, BORSUK_1:43; s2 in dom g by A12, A13, BORSUK_1:43; then s2 = r3 by A11, A18, A20, A21, A23, FUNCT_1:def_4; hence s1 <= s2 by A9, A17, A22, A24, A14, A23, FUNCT_1:def_4; ::_thesis: verum end; q in P by A3, SPPOL_2:17; hence LE f /. i,q, L~ f,f /. 1,f /. (len f) by A5, A6, Def3; ::_thesis: verum end; theorem Th26: :: JORDAN5C:26 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) implies LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) ) assume that A1: f is being_S-Seq and A2: ( 1 <= i & i + 1 <= len f ) and A3: q in LSeg (f,i) ; ::_thesis: LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) len f >= 2 by A1, TOPREAL1:def_8; then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23; set p1 = f /. 1; set p2 = f /. (len f); set q1 = f /. (i + 1); f /. (i + 1) in LSeg (f,i) by A2, TOPREAL1:21; then A4: f /. (i + 1) in P by SPPOL_2:17; A5: for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds s1 <= s2 proof let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A6: g is being_homeomorphism and A7: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and A8: g . s1 = q and A9: ( 0 <= s1 & s1 <= 1 ) and A10: g . s2 = f /. (i + 1) and A11: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 A12: dom g = [#] I[01] by A6, TOPS_2:def_5 .= the carrier of I[01] ; then A13: s2 in dom g by A11, BORSUK_1:43; consider r1, r2 being Real such that A14: ( r1 < r2 & 0 <= r1 ) and r1 <= 1 and 0 <= r2 and A15: r2 <= 1 and A16: LSeg (f,i) = g .: [.r1,r2.] and g . r1 = f /. i and A17: g . r2 = f /. (i + 1) by A1, A2, A6, A7, JORDAN5B:7; A18: r2 in dom g by A14, A15, A12, BORSUK_1:43; consider r39 being set such that A19: r39 in dom g and A20: r39 in [.r1,r2.] and A21: g . r39 = q by A3, A16, FUNCT_1:def_6; r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by A20, RCOMP_1:def_1; then consider r3 being Real such that A22: r3 = r39 and r1 <= r3 and A23: r3 <= r2 ; A24: g is one-to-one by A6, TOPS_2:def_5; s1 in dom g by A9, A12, BORSUK_1:43; then s1 = r3 by A8, A19, A21, A22, A24, FUNCT_1:def_4; hence s1 <= s2 by A10, A17, A23, A18, A13, A24, FUNCT_1:def_4; ::_thesis: verum end; q in P by A3, SPPOL_2:17; hence LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5, Def3; ::_thesis: verum end; theorem :: JORDAN5C:27 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) let q be Point of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) let i, j be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) ) assume that A1: L~ f meets Q and A2: f is being_S-Seq and A3: Q is closed and A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and A5: 1 <= i and A6: i + 1 <= len f and A7: q in LSeg (f,j) and A8: ( 1 <= j & j + 1 <= len f ) and A9: q in Q and A10: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; ::_thesis: ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A4, SPPOL_2:17; set q1 = First_Point (P,(f /. 1),(f /. (len f)),Q); set p1 = f /. i; A11: q in L~ f by A7, SPPOL_2:17; thus i <= j ::_thesis: ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) proof (L~ f) /\ Q is closed by A3, TOPS_1:8; then A12: LE First_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A2, A9, A11, Th15; A13: LE q,f /. (j + 1),P,f /. 1,f /. (len f) by A2, A7, A8, Th26; i <= i + 1 by NAT_1:11; then A14: i <= len f by A6, XXREAL_0:2; assume j < i ; ::_thesis: contradiction then A15: j + 1 <= i by NAT_1:13; 1 <= j + 1 by NAT_1:11; then LE f /. (j + 1),f /. i,P,f /. 1,f /. (len f) by A2, A15, A14, Th24; then A16: LE q,f /. i,P,f /. 1,f /. (len f) by A13, Th13; LE f /. i, First_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A4, A5, A6, Th25; then LE q, First_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A16, Th13; hence contradiction by A2, A10, A12, Th12, TOPREAL1:25; ::_thesis: verum end; assume i = j ; ::_thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) by A1, A2, A3, A4, A5, A6, A7, A9, Lm2; ::_thesis: verum end; theorem :: JORDAN5C:28 for f being FinSequence of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) let q be Point of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) let i, j be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) ) assume that A1: L~ f meets Q and A2: f is being_S-Seq and A3: Q is closed and A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and A5: ( 1 <= i & i + 1 <= len f ) and A6: q in LSeg (f,j) and A7: 1 <= j and A8: j + 1 <= len f and A9: q in Q and A10: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; ::_thesis: ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A4, SPPOL_2:17; set q1 = Last_Point (P,(f /. 1),(f /. (len f)),Q); set p2 = f /. (i + 1); A11: q in L~ f by A6, SPPOL_2:17; thus i >= j ::_thesis: ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) proof assume j > i ; ::_thesis: contradiction then A12: i + 1 <= j by NAT_1:13; j <= j + 1 by NAT_1:11; then ( 1 <= i + 1 & j <= len f ) by A8, NAT_1:11, XXREAL_0:2; then A13: LE f /. (i + 1),f /. j,P,f /. 1,f /. (len f) by A2, A12, Th24; LE f /. j,q,P,f /. 1,f /. (len f) by A2, A6, A7, A8, Th25; then A14: LE f /. (i + 1),q,P,f /. 1,f /. (len f) by A13, Th13; (L~ f) /\ Q is closed by A3, TOPS_1:8; then A15: LE q, Last_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A9, A11, Th16; LE Last_Point (P,(f /. 1),(f /. (len f)),Q),f /. (i + 1),P,f /. 1,f /. (len f) by A2, A4, A5, Th26; then LE Last_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A14, Th13; hence contradiction by A2, A10, A15, Th12, TOPREAL1:25; ::_thesis: verum end; assume i = j ; ::_thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) by A1, A2, A3, A4, A5, A6, A9, Lm4; ::_thesis: verum end; theorem Th29: :: JORDAN5C:29 for f being FinSequence of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for q1, q2 being Point of (TOP-REAL 2) for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) let q1, q2 be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) let i be Element of NAT ; ::_thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) implies LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) ) assume that A1: q1 in LSeg (f,i) and A2: q2 in LSeg (f,i) and A3: f is being_S-Seq and A4: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: ( not LE q1,q2, L~ f,f /. 1,f /. (len f) or LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) ) len f >= 2 by A3, TOPREAL1:def_8; then reconsider P = L~ f, Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:23; L~ f is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25; then consider F being Function of I[01],((TOP-REAL 2) | P) such that A5: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) ) by TOPREAL1:def_1; consider ppi, pi1 being Real such that A6: ppi < pi1 and A7: 0 <= ppi and ppi <= 1 and 0 <= pi1 and A8: pi1 <= 1 and A9: LSeg (f,i) = F .: [.ppi,pi1.] and A10: F . ppi = f /. i and A11: F . pi1 = f /. (i + 1) by A3, A4, A5, JORDAN5B:7; set Ex = L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))); A12: L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is being_homeomorphism by A6, TREAL_1:17; then A13: rng (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) = [#] (Closed-Interval-TSpace (ppi,pi1)) by TOPS_2:def_5; A14: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A6; then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A7, A8, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34; consider G being Function of (I[01] | Poz),((TOP-REAL 2) | Q) such that A15: G = F | Poz and A16: G is being_homeomorphism by A3, A4, A5, A9, JORDAN5B:8; A17: ppi in [.ppi,pi1.] by A14, RCOMP_1:def_1; set H = G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))); A18: dom G = [#] (I[01] | Poz) by A16, TOPS_2:def_5 .= Poz by PRE_TOPC:def_5 .= [#] (Closed-Interval-TSpace (ppi,pi1)) by A6, TOPMETR:18 ; then A19: rng (G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))))) = rng G by A13, RELAT_1:28 .= [#] ((TOP-REAL 2) | (LSeg (f,i))) by A16, TOPS_2:def_5 ; pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A6; then A20: pi1 in [.ppi,pi1.] by RCOMP_1:def_1; A21: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 1 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((0,1) (#)) by TREAL_1:def_2 .= (ppi,pi1) (#) by A6, TREAL_1:9 .= pi1 by A6, TREAL_1:def_2 ; A22: dom (G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))))) = dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, RELAT_1:27 .= [#] I[01] by A12, TOPMETR:20, TOPS_2:def_5 .= the carrier of I[01] ; then reconsider H = G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) as Function of I[01],((TOP-REAL 2) | Q) by A19, FUNCT_2:2; q1 in rng H by A1, A19, PRE_TOPC:def_5; then consider x19 being set such that A23: x19 in dom H and A24: q1 = H . x19 by FUNCT_1:def_3; x19 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A22, A23, BORSUK_1:40, RCOMP_1:def_1; then consider x1 being Real such that A25: x1 = x19 and A26: ( 0 <= x1 & x1 <= 1 ) ; assume A27: LE q1,q2, L~ f,f /. 1,f /. (len f) ; ::_thesis: LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) x1 in the carrier of I[01] by A26, BORSUK_1:43; then x1 in dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, A22, RELAT_1:27; then (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def_3; then A28: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in Poz by A6, TOPMETR:18; 1 in dom H by A22, BORSUK_1:43; then A29: H . 1 = G . pi1 by A21, FUNCT_1:12 .= f /. (i + 1) by A11, A20, A15, FUNCT_1:49 ; A30: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 0 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((#) (0,1)) by TREAL_1:def_1 .= (#) (ppi,pi1) by A6, TREAL_1:9 .= ppi by A6, TREAL_1:def_1 ; q2 in rng H by A2, A19, PRE_TOPC:def_5; then consider x29 being set such that A31: x29 in dom H and A32: q2 = H . x29 by FUNCT_1:def_3; x29 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A22, A31, BORSUK_1:40, RCOMP_1:def_1; then consider x2 being Real such that A33: x2 = x29 and A34: 0 <= x2 and A35: x2 <= 1 ; reconsider X1 = x1, X2 = x2 as Point of (Closed-Interval-TSpace (0,1)) by A26, A34, A35, BORSUK_1:43, TOPMETR:20; x2 in the carrier of I[01] by A34, A35, BORSUK_1:43; then x2 in dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, A22, RELAT_1:27; then (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def_3; then A36: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in Poz by A6, TOPMETR:18; then reconsider E1 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X1, E2 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X2 as Real by A28; A37: q2 = G . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by A31, A32, A33, FUNCT_1:12 .= F . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by A15, A36, FUNCT_1:49 ; reconsider K1 = Closed-Interval-TSpace (ppi,pi1), K2 = I[01] | Poz as SubSpace of I[01] by A6, A7, A8, TOPMETR:20, TREAL_1:3; A38: ( L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is one-to-one & L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is continuous ) by A12, TOPS_2:def_5; the carrier of K1 = [.ppi,pi1.] by A6, TOPMETR:18 .= [#] (I[01] | Poz) by PRE_TOPC:def_5 .= the carrier of K2 ; then I[01] | Poz = Closed-Interval-TSpace (ppi,pi1) by TSEP_1:5; then A39: H is being_homeomorphism by A16, A12, TOPMETR:20, TOPS_2:57; A40: q1 = G . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by A23, A24, A25, FUNCT_1:12 .= F . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by A15, A28, FUNCT_1:49 ; A41: ( 0 <= E2 & E2 <= 1 ) by A36, BORSUK_1:43; 0 in dom H by A22, BORSUK_1:43; then A42: H . 0 = G . ppi by A30, FUNCT_1:12 .= f /. i by A10, A17, A15, FUNCT_1:49 ; E1 <= 1 by A28, BORSUK_1:43; then E1 <= E2 by A27, A5, A40, A37, A41, Def3; then x1 <= x2 by A6, A30, A21, A38, JORDAN5A:15; hence LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) by A3, A4, A39, A42, A29, A24, A32, A25, A26, A33, A35, Th8, JORDAN5B:15; ::_thesis: verum end; theorem :: JORDAN5C:30 for f being FinSequence of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 holds ( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 holds ( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) let q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 implies ( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) ) set p3 = f /. 1; set p4 = f /. (len f); assume that A1: q1 in L~ f and A2: q2 in L~ f and A3: f is being_S-Seq and A4: q1 <> q2 ; ::_thesis: ( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A1; hereby ::_thesis: ( ( for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) implies LE q1,q2, L~ f,f /. 1,f /. (len f) ) assume A5: LE q1,q2, L~ f,f /. 1,f /. (len f) ; ::_thesis: for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) thus for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ::_thesis: verum proof let i, j be Element of NAT ; ::_thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f implies ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) assume that A6: q1 in LSeg (f,i) and A7: q2 in LSeg (f,j) and A8: 1 <= i and A9: i + 1 <= len f and A10: ( 1 <= j & j + 1 <= len f ) ; ::_thesis: ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) thus i <= j ::_thesis: ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) proof assume j < i ; ::_thesis: contradiction then j + 1 <= i by NAT_1:13; then consider m being Nat such that A11: (j + 1) + m = i by NAT_1:10; A12: LE q2,f /. (j + 1),P,f /. 1,f /. (len f) by A3, A7, A10, Th26; reconsider m = m as Element of NAT by ORDINAL1:def_12; A13: ( 1 <= j + 1 & j + 1 <= (j + 1) + m ) by NAT_1:11; i <= i + 1 by NAT_1:11; then (j + 1) + m <= len f by A9, A11, XXREAL_0:2; then LE f /. (j + 1),f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A3, A13, Th24; then A14: LE q2,f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A12, Th13; LE f /. ((j + 1) + m),q1,P,f /. 1,f /. (len f) by A3, A6, A8, A9, A11, Th25; then LE q2,q1,P,f /. 1,f /. (len f) by A14, Th13; hence contradiction by A3, A4, A5, Th12, TOPREAL1:25; ::_thesis: verum end; assume A15: i = j ; ::_thesis: LE q1,q2,f /. i,f /. (i + 1) A16: f is one-to-one by A3, TOPREAL1:def_8; set p1 = f /. i; set p2 = f /. (i + 1); A17: ( i in dom f & i + 1 in dom f ) by A8, A9, SEQ_4:134; A18: f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A17, A16, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A8, A9, TOPREAL1:def_3; hence LE q1,q2,f /. i,f /. (i + 1) by A3, A5, A6, A7, A8, A9, A15, A18, Th17, Th29; ::_thesis: verum end; end; consider i being Element of NAT such that A19: ( 1 <= i & i + 1 <= len f ) and A20: q1 in LSeg (f,i) by A1, SPPOL_2:13; consider j being Element of NAT such that A21: 1 <= j and A22: j + 1 <= len f and A23: q2 in LSeg (f,j) by A2, SPPOL_2:13; assume A24: for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ; ::_thesis: LE q1,q2, L~ f,f /. 1,f /. (len f) then A25: i <= j by A19, A20, A21, A22, A23; percases ( i < j or i = j ) by A25, XXREAL_0:1; suppose i < j ; ::_thesis: LE q1,q2, L~ f,f /. 1,f /. (len f) then i + 1 <= j by NAT_1:13; then consider m being Nat such that A26: j = (i + 1) + m by NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; A27: ( 1 <= i + 1 & i + 1 <= (i + 1) + m ) by NAT_1:11; A28: LE q1,f /. (i + 1),P,f /. 1,f /. (len f) by A3, A19, A20, Th26; j <= j + 1 by NAT_1:11; then (i + 1) + m <= len f by A22, A26, XXREAL_0:2; then LE f /. (i + 1),f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A3, A27, Th24; then A29: LE q1,f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A28, Th13; LE f /. ((i + 1) + m),q2,P,f /. 1,f /. (len f) by A3, A21, A22, A23, A26, Th25; hence LE q1,q2, L~ f,f /. 1,f /. (len f) by A29, Th13; ::_thesis: verum end; supposeA30: i = j ; ::_thesis: LE q1,q2, L~ f,f /. 1,f /. (len f) reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A20; set p1 = f /. i; set p2 = f /. (i + 1); A31: f is one-to-one by A3, TOPREAL1:def_8; A32: ( i in dom f & i + 1 in dom f ) by A19, SEQ_4:134; f /. i <> f /. (i + 1) proof assume f /. i = f /. (i + 1) ; ::_thesis: contradiction then i = i + 1 by A32, A31, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; then consider H being Function of I[01],((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))) such that A33: for x being Real st x in [.0,1.] holds H . x = ((1 - x) * (f /. i)) + (x * (f /. (i + 1))) and A34: H is being_homeomorphism and H . 0 = f /. i and H . 1 = f /. (i + 1) by JORDAN5A:3; A35: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A19, TOPREAL1:def_3; then reconsider H = H as Function of I[01],((TOP-REAL 2) | Q) ; A36: LE q1,q2,f /. i,f /. (i + 1) by A24, A19, A20, A23, A30; ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2 ) ) proof A37: rng H = [#] ((TOP-REAL 2) | (LSeg (f,i))) by A34, A35, TOPS_2:def_5 .= LSeg (f,i) by PRE_TOPC:def_5 ; then consider x19 being set such that A38: x19 in dom H and A39: H . x19 = q1 by A20, FUNCT_1:def_3; A40: dom H = [#] I[01] by A34, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then x19 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A38, RCOMP_1:def_1; then consider x1 being Real such that A41: x1 = x19 and 0 <= x1 and A42: x1 <= 1 ; consider x29 being set such that A43: x29 in dom H and A44: H . x29 = q2 by A23, A30, A37, FUNCT_1:def_3; x29 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A40, A43, RCOMP_1:def_1; then consider x2 being Real such that A45: x2 = x29 and A46: ( 0 <= x2 & x2 <= 1 ) ; A47: q2 = ((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) by A33, A40, A43, A44, A45; q1 = ((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) by A33, A40, A38, A39, A41; then A48: x1 <= x2 by A36, A42, A46, A47, JORDAN3:def_5; 0 in { l where l is Real : ( 0 <= l & l <= 1 ) } ; then A49: 0 in [.0,1.] by RCOMP_1:def_1; then A50: H . 0 = ((1 - 0) * (f /. i)) + (0 * (f /. (i + 1))) by A33 .= (f /. i) + (0 * (f /. (i + 1))) by EUCLID:29 .= (f /. i) + (0. (TOP-REAL 2)) by EUCLID:29 .= f /. i by EUCLID:27 ; thus ( q1 in P & q2 in P ) by A1, A2; ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P) for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2 let F be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 holds s1 <= s2 let s1, s2 be Real; ::_thesis: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 ) assume that A51: F is being_homeomorphism and A52: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) and A53: F . s1 = q1 and A54: ( 0 <= s1 & s1 <= 1 ) and A55: F . s2 = q2 and A56: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2 consider ppi, pi1 being Real such that A57: ppi < pi1 and A58: 0 <= ppi and ppi <= 1 and 0 <= pi1 and A59: pi1 <= 1 and A60: LSeg (f,i) = F .: [.ppi,pi1.] and A61: F . ppi = f /. i and A62: F . pi1 = f /. (i + 1) by A3, A19, A51, A52, JORDAN5B:7; A63: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A57; then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A58, A59, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34; consider G being Function of (I[01] | Poz),((TOP-REAL 2) | Q) such that A64: G = F | Poz and A65: G is being_homeomorphism by A3, A19, A51, A52, A60, JORDAN5B:8; A66: dom F = [#] I[01] by A51, TOPS_2:def_5 .= the carrier of I[01] ; reconsider K1 = Closed-Interval-TSpace (ppi,pi1), K2 = I[01] | Poz as SubSpace of I[01] by A57, A58, A59, TOPMETR:20, TREAL_1:3; A67: the carrier of K1 = [.ppi,pi1.] by A57, TOPMETR:18 .= [#] (I[01] | Poz) by PRE_TOPC:def_5 .= the carrier of K2 ; then reconsider E = (G ") * H as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by TOPMETR:20; A68: G is one-to-one by A65, TOPS_2:def_5; reconsider X1 = x1, X2 = x2 as Point of (Closed-Interval-TSpace (0,1)) by A40, A38, A41, A43, A45, TOPMETR:18; A69: G " is being_homeomorphism by A65, TOPS_2:56; A70: s2 in the carrier of I[01] by A56, BORSUK_1:43; A71: F is one-to-one by A51, TOPS_2:def_5; rng G = [#] ((TOP-REAL 2) | (LSeg (f,i))) by A65, TOPS_2:def_5; then G is onto by FUNCT_2:def_3; then A72: G " = G " by A68, TOPS_2:def_4; A73: ex x9 being set st ( x9 in dom F & x9 in [.ppi,pi1.] & q2 = F . x9 ) by A23, A30, A60, FUNCT_1:def_6; then s2 in Poz by A55, A70, A66, A71, FUNCT_1:def_4; then A74: G . s2 = q2 by A55, A64, FUNCT_1:49; dom G = [#] (I[01] | Poz) by A65, TOPS_2:def_5; then A75: dom G = Poz by PRE_TOPC:def_5; then s2 in dom G by A55, A70, A66, A71, A73, FUNCT_1:def_4; then A76: s2 = (G ") . (H . x2) by A44, A45, A68, A72, A74, FUNCT_1:32 .= E . x2 by A43, A45, FUNCT_1:13 ; then A77: s2 = E . X2 ; consider x being set such that A78: x in dom F and A79: x in [.ppi,pi1.] and A80: q1 = F . x by A20, A60, FUNCT_1:def_6; A81: s1 in the carrier of I[01] by A54, BORSUK_1:43; then x = s1 by A53, A66, A71, A78, A80, FUNCT_1:def_4; then A82: G . s1 = q1 by A64, A79, A80, FUNCT_1:49; Closed-Interval-TSpace (ppi,pi1) = I[01] | Poz by A67, TSEP_1:5; then E is being_homeomorphism by A34, A35, A69, TOPMETR:20, TOPS_2:57; then A83: ( E is continuous & E is one-to-one ) by TOPS_2:def_5; 1 in { l where l is Real : ( 0 <= l & l <= 1 ) } ; then A84: 1 in [.0,1.] by RCOMP_1:def_1; then A85: H . 1 = ((1 - 1) * (f /. i)) + (1 * (f /. (i + 1))) by A33 .= (0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) by EUCLID:29 .= (0. (TOP-REAL 2)) + (f /. (i + 1)) by EUCLID:29 .= f /. (i + 1) by EUCLID:27 ; s1 in dom G by A53, A81, A66, A71, A75, A79, A80, FUNCT_1:def_4; then A86: s1 = (G ") . (H . x1) by A39, A41, A68, A72, A82, FUNCT_1:32 .= E . x1 by A38, A41, FUNCT_1:13 ; then A87: s1 = E . X1 ; pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A57; then A88: pi1 in [.ppi,pi1.] by RCOMP_1:def_1; then G . pi1 = f /. (i + 1) by A62, A64, FUNCT_1:49; then A89: pi1 = (G ") . (H . 1) by A88, A68, A75, A72, A85, FUNCT_1:32 .= E . 1 by A40, A84, FUNCT_1:13 ; A90: ppi in [.ppi,pi1.] by A63, RCOMP_1:def_1; then G . ppi = f /. i by A61, A64, FUNCT_1:49; then A91: ppi = (G ") . (H . 0) by A90, A68, A75, A72, A50, FUNCT_1:32 .= E . 0 by A40, A49, FUNCT_1:13 ; percases ( x1 = x2 or x1 < x2 ) by A48, XXREAL_0:1; suppose x1 = x2 ; ::_thesis: s1 <= s2 hence s1 <= s2 by A86, A76; ::_thesis: verum end; suppose x1 < x2 ; ::_thesis: s1 <= s2 hence s1 <= s2 by A57, A83, A91, A89, A87, A77, JORDAN5A:15; ::_thesis: verum end; end; end; hence LE q1,q2, L~ f,f /. 1,f /. (len f) by Def3; ::_thesis: verum end; end; end;