:: JORDAN6 semantic presentation begin theorem Th1: :: JORDAN6:1 for r, s being real number st r <= s holds ( r <= (r + s) / 2 & (r + s) / 2 <= s ) proof let r, s be real number ; ::_thesis: ( r <= s implies ( r <= (r + s) / 2 & (r + s) / 2 <= s ) ) assume A1: r <= s ; ::_thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s ) percases ( r < s or r = s ) by A1, XXREAL_0:1; suppose r < s ; ::_thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s ) hence ( r <= (r + s) / 2 & (r + s) / 2 <= s ) by XREAL_1:226; ::_thesis: verum end; suppose r = s ; ::_thesis: ( r <= (r + s) / 2 & (r + s) / 2 <= s ) hence ( r <= (r + s) / 2 & (r + s) / 2 <= s ) ; ::_thesis: verum end; end; end; theorem Th2: :: JORDAN6:2 for TX being non empty TopSpace for P being Subset of TX for A being Subset of (TX | P) for B being Subset of TX st B is closed & A = B /\ P holds A is closed proof let TX be non empty TopSpace; ::_thesis: for P being Subset of TX for A being Subset of (TX | P) for B being Subset of TX st B is closed & A = B /\ P holds A is closed let P be Subset of TX; ::_thesis: for A being Subset of (TX | P) for B being Subset of TX st B is closed & A = B /\ P holds A is closed let A be Subset of (TX | P); ::_thesis: for B being Subset of TX st B is closed & A = B /\ P holds A is closed let B be Subset of TX; ::_thesis: ( B is closed & A = B /\ P implies A is closed ) assume that A1: B is closed and A2: A = B /\ P ; ::_thesis: A is closed [#] (TX | P) = P by PRE_TOPC:def_5; hence A is closed by A1, A2, PRE_TOPC:13; ::_thesis: verum end; theorem Th3: :: JORDAN6:3 for TX, TY being non empty TopSpace for P being non empty Subset of TY for f being Function of TX,(TY | P) holds ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds f2 is continuous ) ) proof let TX, TY be non empty TopSpace; ::_thesis: for P being non empty Subset of TY for f being Function of TX,(TY | P) holds ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds f2 is continuous ) ) let P be non empty Subset of TY; ::_thesis: for f being Function of TX,(TY | P) holds ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds f2 is continuous ) ) let f be Function of TX,(TY | P); ::_thesis: ( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds f2 is continuous ) ) A1: the carrier of (TY | P) = [#] (TY | P) .= P by PRE_TOPC:def_5 ; hence f is Function of TX,TY by FUNCT_2:7; ::_thesis: for f2 being Function of TX,TY st f2 = f & f is continuous holds f2 is continuous let f2 be Function of TX,TY; ::_thesis: ( f2 = f & f is continuous implies f2 is continuous ) assume that A2: f2 = f and A3: f is continuous ; ::_thesis: f2 is continuous let P1 be Subset of TY; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f2 " P1 is closed ) assume A4: P1 is closed ; ::_thesis: f2 " P1 is closed reconsider P3 = P1 /\ P as Subset of (TY | P) by TOPS_2:29; A5: P3 is closed by A4, Th2; f2 " P = the carrier of TX by A1, A2, FUNCT_2:40 .= dom f2 by FUNCT_2:def_1 ; then f2 " P1 = (f2 " P1) /\ (f2 " P) by RELAT_1:132, XBOOLE_1:28 .= f " P3 by A2, FUNCT_1:68 ; hence f2 " P1 is closed by A3, A5, PRE_TOPC:def_6; ::_thesis: verum end; theorem Th4: :: JORDAN6:4 for r being real number for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds P is closed proof let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds P is closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } implies P is closed ) assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } ; ::_thesis: P is closed A2: 1 in Seg 2 by FINSEQ_1:1; A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `1 < r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `1 < r } ) assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `1 < r } then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4; then A5: not x in P by XBOOLE_0:def_5; reconsider q = x as Point of (TOP-REAL 2) by A4; q `1 < r by A1, A5; hence x in { p where p is Point of (TOP-REAL 2) : p `1 < r } ; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : p `1 < r } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 < r } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : p `1 < r } ; ::_thesis: x in P ` then A6: ex p being Point of (TOP-REAL 2) st ( p = x & p `1 < r ) ; now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`1_>=_r__}_ assume x in { q where q is Point of (TOP-REAL 2) : q `1 >= r } ; ::_thesis: contradiction then ex q being Point of (TOP-REAL 2) st ( q = x & q `1 >= r ) ; hence contradiction by A6; ::_thesis: verum end; then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5; hence x in P ` by SUBSET_1:def_4; ::_thesis: verum end; then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `1 < r } by A3, XBOOLE_0:def_10; A8: P ` c= { p where p is Point of (TOP-REAL 2) : r > p /. 1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } ) assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } then consider p being Point of (TOP-REAL 2) such that A9: p = x and A10: p `1 < r by A7; p /. 1 < r by A10, JORDAN2B:29; hence x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } by A9; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : r > p /. 1 } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : r > p /. 1 } ; ::_thesis: x in P ` then consider q being Point of (TOP-REAL 2) such that A11: q = x and A12: r > q /. 1 ; q `1 < r by A12, JORDAN2B:29; hence x in P ` by A7, A11; ::_thesis: verum end; then A13: P ` = { p where p is Point of (TOP-REAL 2) : r > p /. 1 } by A8, XBOOLE_0:def_10; reconsider P1 = P ` as Subset of (TOP-REAL 2) ; P1 is open by A2, A13, JORDAN2B:12; hence P is closed by TOPS_1:3; ::_thesis: verum end; theorem Th5: :: JORDAN6:5 for r being real number for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds P is closed proof let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds P is closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } implies P is closed ) assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } ; ::_thesis: P is closed A2: 1 in Seg 2 by FINSEQ_1:1; A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `1 > r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ) assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `1 > r } then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4; then A5: not x in P by XBOOLE_0:def_5; reconsider q = x as Point of (TOP-REAL 2) by A4; q `1 > r by A1, A5; hence x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : p `1 > r } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 > r } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : p `1 > r } ; ::_thesis: x in P ` then A6: ex p being Point of (TOP-REAL 2) st ( p = x & p `1 > r ) ; now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`1_<=_r__}_ assume x in { q where q is Point of (TOP-REAL 2) : q `1 <= r } ; ::_thesis: contradiction then ex q being Point of (TOP-REAL 2) st ( q = x & q `1 <= r ) ; hence contradiction by A6; ::_thesis: verum end; then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5; hence x in P ` by SUBSET_1:def_4; ::_thesis: verum end; then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `1 > r } by A3, XBOOLE_0:def_10; A8: P ` c= { p where p is Point of (TOP-REAL 2) : r < p /. 1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } ) assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } then consider p being Point of (TOP-REAL 2) such that A9: p = x and A10: p `1 > r by A7; p /. 1 > r by A10, JORDAN2B:29; hence x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } by A9; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : r < p /. 1 } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : r < p /. 1 } ; ::_thesis: x in P ` then consider q being Point of (TOP-REAL 2) such that A11: q = x and A12: r < q /. 1 ; q `1 > r by A12, JORDAN2B:29; hence x in P ` by A7, A11; ::_thesis: verum end; then A13: P ` = { p where p is Point of (TOP-REAL 2) : r < p /. 1 } by A8, XBOOLE_0:def_10; reconsider P1 = P ` as Subset of (TOP-REAL 2) ; P1 is open by A2, A13, JORDAN2B:13; hence P is closed by TOPS_1:3; ::_thesis: verum end; theorem Th6: :: JORDAN6:6 for r being real number for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds P is closed proof let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds P is closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 = r } implies P is closed ) assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 = r } ; ::_thesis: P is closed defpred S1[ Point of (TOP-REAL 2)] means $1 `1 >= r; { p where p is Element of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `1 >= r } as Subset of (TOP-REAL 2) ; A2: P1 is closed by Th4; defpred S2[ Point of (TOP-REAL 2)] means $1 `1 <= r; { p where p is Element of (TOP-REAL 2) : S2[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `1 <= r } as Subset of (TOP-REAL 2) ; A3: P2 is closed by Th5; A4: P c= P1 /\ P2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in P1 /\ P2 ) assume x in P ; ::_thesis: x in P1 /\ P2 then A5: ex p being Point of (TOP-REAL 2) st ( p = x & p `1 = r ) by A1; then A6: x in P1 ; x in P2 by A5; hence x in P1 /\ P2 by A6, XBOOLE_0:def_4; ::_thesis: verum end; P1 /\ P2 c= P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 /\ P2 or x in P ) assume A7: x in P1 /\ P2 ; ::_thesis: x in P then A8: x in P1 by XBOOLE_0:def_4; A9: x in P2 by A7, XBOOLE_0:def_4; consider q1 being Point of (TOP-REAL 2) such that A10: q1 = x and A11: q1 `1 >= r by A8; ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `1 <= r ) by A9; then q1 `1 = r by A10, A11, XXREAL_0:1; hence x in P by A1, A10; ::_thesis: verum end; then P = P1 /\ P2 by A4, XBOOLE_0:def_10; hence P is closed by A2, A3, TOPS_1:8; ::_thesis: verum end; theorem Th7: :: JORDAN6:7 for r being real number for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds P is closed proof let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds P is closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } implies P is closed ) assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } ; ::_thesis: P is closed A2: 2 in Seg 2 by FINSEQ_1:1; A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `2 < r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ) assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `2 < r } then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4; then A5: not x in P by XBOOLE_0:def_5; reconsider q = x as Point of (TOP-REAL 2) by A4; q `2 < r by A1, A5; hence x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : p `2 < r } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `2 < r } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : p `2 < r } ; ::_thesis: x in P ` then A6: ex p being Point of (TOP-REAL 2) st ( p = x & p `2 < r ) ; now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`2_>=_r__}_ assume x in { q where q is Point of (TOP-REAL 2) : q `2 >= r } ; ::_thesis: contradiction then ex q being Point of (TOP-REAL 2) st ( q = x & q `2 >= r ) ; hence contradiction by A6; ::_thesis: verum end; then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5; hence x in P ` by SUBSET_1:def_4; ::_thesis: verum end; then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `2 < r } by A3, XBOOLE_0:def_10; A8: P ` c= { p where p is Point of (TOP-REAL 2) : r > p /. 2 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } ) assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } then consider p being Point of (TOP-REAL 2) such that A9: p = x and A10: p `2 < r by A7; p /. 2 < r by A10, JORDAN2B:29; hence x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } by A9; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : r > p /. 2 } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : r > p /. 2 } ; ::_thesis: x in P ` then consider q being Point of (TOP-REAL 2) such that A11: q = x and A12: r > q /. 2 ; q `2 < r by A12, JORDAN2B:29; hence x in P ` by A7, A11; ::_thesis: verum end; then A13: P ` = { p where p is Point of (TOP-REAL 2) : r > p /. 2 } by A8, XBOOLE_0:def_10; reconsider P1 = P ` as Subset of (TOP-REAL 2) ; P1 is open by A2, A13, JORDAN2B:12; hence P is closed by TOPS_1:3; ::_thesis: verum end; theorem Th8: :: JORDAN6:8 for r being real number for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds P is closed proof let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds P is closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } implies P is closed ) assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } ; ::_thesis: P is closed A2: 2 in Seg 2 by FINSEQ_1:1; A3: P ` c= { p where p is Point of (TOP-REAL 2) : p `2 > r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : p `2 > r } ) assume A4: x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : p `2 > r } then x in the carrier of (TOP-REAL 2) \ P by SUBSET_1:def_4; then A5: not x in P by XBOOLE_0:def_5; reconsider q = x as Point of (TOP-REAL 2) by A4; q `2 > r by A1, A5; hence x in { p where p is Point of (TOP-REAL 2) : p `2 > r } ; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : p `2 > r } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `2 > r } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : p `2 > r } ; ::_thesis: x in P ` then A6: ex p being Point of (TOP-REAL 2) st ( p = x & p `2 > r ) ; now__::_thesis:_not_x_in__{__q_where_q_is_Point_of_(TOP-REAL_2)_:_q_`2_<=_r__}_ assume x in { q where q is Point of (TOP-REAL 2) : q `2 <= r } ; ::_thesis: contradiction then ex q being Point of (TOP-REAL 2) st ( q = x & q `2 <= r ) ; hence contradiction by A6; ::_thesis: verum end; then x in the carrier of (TOP-REAL 2) \ P by A1, A6, XBOOLE_0:def_5; hence x in P ` by SUBSET_1:def_4; ::_thesis: verum end; then A7: P ` = { p where p is Point of (TOP-REAL 2) : p `2 > r } by A3, XBOOLE_0:def_10; A8: P ` c= { p where p is Point of (TOP-REAL 2) : r < p /. 2 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P ` or x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } ) assume x in P ` ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } then consider p being Point of (TOP-REAL 2) such that A9: p = x and A10: p `2 > r by A7; p /. 2 > r by A10, JORDAN2B:29; hence x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } by A9; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : r < p /. 2 } c= P ` proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } or x in P ` ) assume x in { p where p is Point of (TOP-REAL 2) : r < p /. 2 } ; ::_thesis: x in P ` then consider q being Point of (TOP-REAL 2) such that A11: q = x and A12: r < q /. 2 ; q `2 > r by A12, JORDAN2B:29; hence x in P ` by A7, A11; ::_thesis: verum end; then A13: P ` = { p where p is Point of (TOP-REAL 2) : r < p /. 2 } by A8, XBOOLE_0:def_10; reconsider P1 = P ` as Subset of (TOP-REAL 2) ; P1 is open by A2, A13, JORDAN2B:13; hence P is closed by TOPS_1:3; ::_thesis: verum end; theorem Th9: :: JORDAN6:9 for r being real number for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds P is closed proof let r be real number ; ::_thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds P is closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `2 = r } implies P is closed ) assume A1: P = { p where p is Point of (TOP-REAL 2) : p `2 = r } ; ::_thesis: P is closed defpred S1[ Point of (TOP-REAL 2)] means $1 `2 >= r; { p where p is Element of (TOP-REAL 2) : S1[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `2 >= r } as Subset of (TOP-REAL 2) ; A2: P1 is closed by Th7; defpred S2[ Point of (TOP-REAL 2)] means $1 `2 <= r; { p where p is Element of (TOP-REAL 2) : S2[p] } is Subset of (TOP-REAL 2) from DOMAIN_1:sch_7(); then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `2 <= r } as Subset of (TOP-REAL 2) ; A3: P2 is closed by Th8; A4: P c= P1 /\ P2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in P1 /\ P2 ) assume x in P ; ::_thesis: x in P1 /\ P2 then A5: ex p being Point of (TOP-REAL 2) st ( p = x & p `2 = r ) by A1; then A6: x in P1 ; x in P2 by A5; hence x in P1 /\ P2 by A6, XBOOLE_0:def_4; ::_thesis: verum end; P1 /\ P2 c= P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 /\ P2 or x in P ) assume A7: x in P1 /\ P2 ; ::_thesis: x in P then A8: x in P1 by XBOOLE_0:def_4; A9: x in P2 by A7, XBOOLE_0:def_4; consider q1 being Point of (TOP-REAL 2) such that A10: q1 = x and A11: q1 `2 >= r by A8; ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `2 <= r ) by A9; then q1 `2 = r by A10, A11, XXREAL_0:1; hence x in P by A1, A10; ::_thesis: verum end; then P = P1 /\ P2 by A4, XBOOLE_0:def_10; hence P is closed by A2, A3, TOPS_1:8; ::_thesis: verum end; theorem Th10: :: JORDAN6:10 for n being Element of NAT for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P is connected proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P is connected let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P is connected let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies P is connected ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: P is connected then consider f being Function of I[01],((TOP-REAL n) | P) such that A2: f is being_homeomorphism and f . 0 = p1 and f . 1 = p2 by TOPREAL1:def_1; reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1; A3: f is continuous Function of I[01],((TOP-REAL n) | P9) by A2, TOPS_2:def_5; A4: [#] I[01] is connected by CONNSP_1:27, TREAL_1:19; A5: rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def_5; A6: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def_5; dom f = [#] I[01] by A2, TOPS_2:def_5; then A7: P = f .: ([#] I[01]) by A5, A6, RELAT_1:113; f .: ([#] I[01]) is connected by A3, A4, TOPS_2:61; hence P is connected by A7, CONNSP_1:23; ::_thesis: verum end; theorem :: JORDAN6: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 P is closed by COMPTS_1:7, JORDAN5A:1; theorem Th12: :: JORDAN6:12 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 ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) 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 ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) then A2: p1 in P by TOPREAL1:1; reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1; consider f being Function of I[01],((TOP-REAL 2) | P9) such that A3: f is being_homeomorphism and A4: f . 0 = p1 and A5: f . 1 = p2 by A1, TOPREAL1:def_1; A6: f is continuous by A3, TOPS_2:def_5; consider h being Function of (TOP-REAL 2),R^1 such that A7: for p being Element of (TOP-REAL 2) holds h . p = p /. 1 by JORDAN2B:1; 1 in Seg 2 by FINSEQ_1:1; then A8: h is continuous by A7, JORDAN2B:18; A9: the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P) .= P9 by PRE_TOPC:def_5 ; then A10: f is Function of the carrier of I[01], the carrier of (TOP-REAL 2) by FUNCT_2:7; reconsider f1 = f as Function of I[01],(TOP-REAL 2) by A9, FUNCT_2:7; A11: f1 is continuous by A6, Th3; reconsider g = h * f as Function of I[01],R^1 by A10; A12: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1; then A13: 0 in dom f by XXREAL_1:1; A14: 1 in dom f by A12, XXREAL_1:1; A15: g . 0 = h . (f . 0) by A13, FUNCT_1:13 .= p1 /. 1 by A4, A7 .= p1 `1 by JORDAN2B:29 ; A16: g . 1 = h . (f . 1) by A14, FUNCT_1:13 .= p2 /. 1 by A5, A7 .= p2 `1 by JORDAN2B:29 ; percases ( g . 0 <> g . 1 or g . 0 = g . 1 ) ; suppose g . 0 <> g . 1 ; ::_thesis: ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) then consider r1 being Real such that A17: 0 < r1 and A18: r1 < 1 and A19: g . r1 = ((p1 `1) + (p2 `1)) / 2 by A8, A11, A15, A16, TOPREAL5:9; A20: r1 in [.0,1.] by A17, A18, XXREAL_1:1; A21: r1 in the carrier of I[01] by A17, A18, BORSUK_1:40, XXREAL_1:1; then reconsider q1 = f . r1 as Point of (TOP-REAL 2) by A10, FUNCT_2:5; g . r1 = h . (f . r1) by A12, A20, FUNCT_1:13 .= q1 /. 1 by A7 .= q1 `1 by JORDAN2B:29 ; hence ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) by A9, A19, A21, FUNCT_2:5; ::_thesis: verum end; suppose g . 0 = g . 1 ; ::_thesis: ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) hence ex q being Point of (TOP-REAL 2) st ( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 ) by A2, A15, A16; ::_thesis: verum end; end; end; theorem Th13: :: JORDAN6:13 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 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds ( P meets Q & P /\ Q is closed ) 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 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds ( P meets Q & P /\ Q is closed ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies ( P meets Q & P /\ Q is closed ) ) reconsider W = P as Subset of (TOP-REAL 2) ; assume A1: ( P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ) ; ::_thesis: ( P meets Q & P /\ Q is closed ) consider f being Function of (TOP-REAL 2),R^1 such that A2: for p being Element of (TOP-REAL 2) holds f . p = p /. 1 by JORDAN2B:1; reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1; A3: 1 in Seg 2 by FINSEQ_1:1; A4: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; A5: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; then A6: the carrier of ((TOP-REAL 2) | P9) = P9 ; A7: dom (f | P) = the carrier of (TOP-REAL 2) /\ P by A4, RELAT_1:61 .= P by XBOOLE_1:28 ; rng (f | P) c= the carrier of R^1 ; then reconsider g = f | P as Function of ((TOP-REAL 2) | P),R^1 by A5, A7, FUNCT_2:def_1, RELSET_1:4; reconsider g = g as continuous Function of ((TOP-REAL 2) | P9),R^1 by A2, A3, JORDAN2B:18, TOPMETR:7; A8: p1 in P by A1, TOPREAL1:1; A9: p2 in P by A1, TOPREAL1:1; reconsider p19 = p1, p29 = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:1; A10: g . p19 = f . p1 by A8, FUNCT_1:49 .= p1 /. 1 by A2 .= p1 `1 by JORDAN2B:29 ; A11: g . p29 = f . p2 by A9, FUNCT_1:49 .= p2 /. 1 by A2 .= p2 `1 by JORDAN2B:29 ; W is connected by A1, Th10; then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def_3; A13: now__::_thesis:_(_(_p1_`1_<=_p2_`1_&_P_meets_Q_)_or_(_p1_`1_>_p2_`1_&_P_meets_Q_)_) percases ( p1 `1 <= p2 `1 or p1 `1 > p2 `1 ) ; caseA14: p1 `1 <= p2 `1 ; ::_thesis: P meets Q then A15: p1 `1 <= ((p1 `1) + (p2 `1)) / 2 by Th1; ((p1 `1) + (p2 `1)) / 2 <= p2 `1 by A14, Th1; then consider xc being Point of ((TOP-REAL 2) | P) such that A16: g . xc = ((p1 `1) + (p2 `1)) / 2 by A10, A11, A12, A15, TOPREAL5:4; xc in P by A6; then reconsider pc = xc as Point of (TOP-REAL 2) ; g . xc = f . xc by A5, FUNCT_1:49 .= pc /. 1 by A2 .= pc `1 by JORDAN2B:29 ; then xc in Q by A1, A16; hence P meets Q by A6, XBOOLE_0:3; ::_thesis: verum end; caseA17: p1 `1 > p2 `1 ; ::_thesis: P meets Q then A18: p2 `1 <= ((p1 `1) + (p2 `1)) / 2 by Th1; ((p1 `1) + (p2 `1)) / 2 <= p1 `1 by A17, Th1; then consider xc being Point of ((TOP-REAL 2) | P) such that A19: g . xc = ((p1 `1) + (p2 `1)) / 2 by A10, A11, A12, A18, TOPREAL5:4; xc in P by A6; then reconsider pc = xc as Point of (TOP-REAL 2) ; g . xc = f . xc by A5, FUNCT_1:49 .= pc /. 1 by A2 .= pc `1 by JORDAN2B:29 ; then xc in Q by A1, A19; hence P meets Q by A6, XBOOLE_0:3; ::_thesis: verum end; end; end; reconsider P1 = P, Q1 = Q as Subset of (TOP-REAL 2) ; A20: P1 is closed by A1, COMPTS_1:7, JORDAN5A:1; Q1 is closed by A1, Th6; hence ( P meets Q & P /\ Q is closed ) by A13, A20, TOPS_1:8; ::_thesis: verum end; theorem Th14: :: JORDAN6:14 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 & Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds ( P meets Q & P /\ Q is closed ) proof let P, Q1 be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds ( P meets Q1 & P /\ Q1 is closed ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies ( P meets Q1 & P /\ Q1 is closed ) ) assume A1: ( P is_an_arc_of p1,p2 & Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ) ; ::_thesis: ( P meets Q1 & P /\ Q1 is closed ) consider f being Function of (TOP-REAL 2),R^1 such that A2: for p being Element of (TOP-REAL 2) holds f . p = p /. 2 by JORDAN2B:1; reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1; A3: 2 in Seg 2 by FINSEQ_1:1; A4: dom f = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; A5: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; then A6: the carrier of ((TOP-REAL 2) | P9) = P9 ; A7: dom (f | P) = the carrier of (TOP-REAL 2) /\ P by A4, RELAT_1:61 .= P by XBOOLE_1:28 ; rng (f | P) c= the carrier of R^1 ; then reconsider g = f | P as Function of ((TOP-REAL 2) | P),R^1 by A5, A7, FUNCT_2:def_1, RELSET_1:4; reconsider g = g as continuous Function of ((TOP-REAL 2) | P9),R^1 by A2, A3, JORDAN2B:18, TOPMETR:7; A8: p1 in P by A1, TOPREAL1:1; A9: p2 in P by A1, TOPREAL1:1; reconsider p19 = p1, p29 = p2 as Point of ((TOP-REAL 2) | P) by A1, A5, TOPREAL1:1; A10: g . p19 = f . p1 by A8, FUNCT_1:49 .= p1 /. 2 by A2 .= p1 `2 by JORDAN2B:29 ; A11: g . p29 = f . p2 by A9, FUNCT_1:49 .= p2 /. 2 by A2 .= p2 `2 by JORDAN2B:29 ; reconsider W = P as Subset of (TOP-REAL 2) ; W is connected by A1, Th10; then A12: (TOP-REAL 2) | P is connected by CONNSP_1:def_3; A13: now__::_thesis:_(_(_p1_`2_<=_p2_`2_&_P_meets_Q1_)_or_(_p1_`2_>_p2_`2_&_P_meets_Q1_)_) percases ( p1 `2 <= p2 `2 or p1 `2 > p2 `2 ) ; caseA14: p1 `2 <= p2 `2 ; ::_thesis: P meets Q1 then A15: p1 `2 <= ((p1 `2) + (p2 `2)) / 2 by Th1; ((p1 `2) + (p2 `2)) / 2 <= p2 `2 by A14, Th1; then consider xc being Point of ((TOP-REAL 2) | P) such that A16: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A15, TOPREAL5:4; xc in P by A6; then reconsider pc = xc as Point of (TOP-REAL 2) ; g . xc = f . xc by A5, FUNCT_1:49 .= pc /. 2 by A2 .= pc `2 by JORDAN2B:29 ; then xc in Q1 by A1, A16; hence P meets Q1 by A6, XBOOLE_0:3; ::_thesis: verum end; caseA17: p1 `2 > p2 `2 ; ::_thesis: P meets Q1 then A18: p2 `2 <= ((p1 `2) + (p2 `2)) / 2 by Th1; ((p1 `2) + (p2 `2)) / 2 <= p1 `2 by A17, Th1; then consider xc being Point of ((TOP-REAL 2) | P) such that A19: g . xc = ((p1 `2) + (p2 `2)) / 2 by A10, A11, A12, A18, TOPREAL5:4; xc in P by A6; then reconsider pc = xc as Point of (TOP-REAL 2) ; g . xc = f . xc by A5, FUNCT_1:49 .= pc /. 2 by A2 .= pc `2 by JORDAN2B:29 ; then xc in Q1 by A1, A19; hence P meets Q1 by A6, XBOOLE_0:3; ::_thesis: verum end; end; end; reconsider P1 = P, Q2 = Q1 as Subset of (TOP-REAL 2) ; A20: P1 is closed by A1, COMPTS_1:7, JORDAN5A:1; Q2 is closed by A1, Th9; hence ( P meets Q1 & P /\ Q1 is closed ) by A13, A20, TOPS_1:8; ::_thesis: verum end; definition let P be Subset of (TOP-REAL 2); let p1, p2 be Point of (TOP-REAL 2); func x_Middle (P,p1,p2) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN6:def 1 for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds it = First_Point (P,p1,p2,Q); existence ex b1 being Point of (TOP-REAL 2) st for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds b1 = First_Point (P,p1,p2,Q) proof { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } or x in the carrier of (TOP-REAL 2) ) assume x in { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q being Point of (TOP-REAL 2) st ( q = x & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider Q1 = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } as Subset of (TOP-REAL 2) ; reconsider q2 = First_Point (P,p1,p2,Q1) as Point of (TOP-REAL 2) ; for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds q2 = First_Point (P,p1,p2,Q) ; hence ex b1 being Point of (TOP-REAL 2) st for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds b1 = First_Point (P,p1,p2,Q) ; ::_thesis: verum end; uniqueness for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds b1 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds b2 = First_Point (P,p1,p2,Q) ) holds b1 = b2 proof let q3, q4 be Point of (TOP-REAL 2); ::_thesis: ( ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds q3 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 ) assume A1: ( ( for Q1 being Subset of (TOP-REAL 2) st Q1 = { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } holds q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of (TOP-REAL 2) st Q2 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `1 = ((p1 `1) + (p2 `1)) / 2 } holds q4 = First_Point (P,p1,p2,Q2) ) ) ; ::_thesis: q3 = q4 { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } or x in the carrier of (TOP-REAL 2) ) assume x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `1 = ((p1 `1) + (p2 `1)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q being Point of (TOP-REAL 2) st ( q = x & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider Q3 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `1 = ((p1 `1) + (p2 `1)) / 2 } as Subset of (TOP-REAL 2) ; q3 = First_Point (P,p1,p2,Q3) by A1; hence q3 = q4 by A1; ::_thesis: verum end; end; :: deftheorem Def1 defines x_Middle JORDAN6:def_1_:_ for P being Subset of (TOP-REAL 2) for p1, p2, b4 being Point of (TOP-REAL 2) holds ( b4 = x_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds b4 = First_Point (P,p1,p2,Q) ); definition let P be Subset of (TOP-REAL 2); let p1, p2 be Point of (TOP-REAL 2); func y_Middle (P,p1,p2) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN6:def 2 for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds it = First_Point (P,p1,p2,Q); existence ex b1 being Point of (TOP-REAL 2) st for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds b1 = First_Point (P,p1,p2,Q) proof { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } or x in the carrier of (TOP-REAL 2) ) assume x in { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q being Point of (TOP-REAL 2) st ( q = x & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider Q1 = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } as Subset of (TOP-REAL 2) ; reconsider q2 = First_Point (P,p1,p2,Q1) as Point of (TOP-REAL 2) ; for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds q2 = First_Point (P,p1,p2,Q) ; hence ex b1 being Point of (TOP-REAL 2) st for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds b1 = First_Point (P,p1,p2,Q) ; ::_thesis: verum end; uniqueness for b1, b2 being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds b1 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds b2 = First_Point (P,p1,p2,Q) ) holds b1 = b2 proof let q3, q4 be Point of (TOP-REAL 2); ::_thesis: ( ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds q3 = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds q4 = First_Point (P,p1,p2,Q) ) implies q3 = q4 ) assume A1: ( ( for Q1 being Subset of (TOP-REAL 2) st Q1 = { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } holds q3 = First_Point (P,p1,p2,Q1) ) & ( for Q2 being Subset of (TOP-REAL 2) st Q2 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `2 = ((p1 `2) + (p2 `2)) / 2 } holds q4 = First_Point (P,p1,p2,Q2) ) ) ; ::_thesis: q3 = q4 { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } or x in the carrier of (TOP-REAL 2) ) assume x in { q1 where q1 is Point of (TOP-REAL 2) : q1 `2 = ((p1 `2) + (p2 `2)) / 2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q being Point of (TOP-REAL 2) st ( q = x & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; then reconsider Q3 = { q2 where q2 is Point of (TOP-REAL 2) : q2 `2 = ((p1 `2) + (p2 `2)) / 2 } as Subset of (TOP-REAL 2) ; q3 = First_Point (P,p1,p2,Q3) by A1; hence q3 = q4 by A1; ::_thesis: verum end; end; :: deftheorem Def2 defines y_Middle JORDAN6:def_2_:_ for P being Subset of (TOP-REAL 2) for p1, p2, b4 being Point of (TOP-REAL 2) holds ( b4 = y_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds b4 = First_Point (P,p1,p2,Q) ); theorem :: JORDAN6:15 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 ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) 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 ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) deffunc H1( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1; defpred S1[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1) + (p2 `1)) / 2; reconsider Q = { H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8(); A2: x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q) by Def1; A3: P meets Q by A1, Th13; P /\ Q is closed by A1, Th13; then A4: x_Middle (P,p1,p2) in P /\ Q by A1, A2, A3, JORDAN5C:def_1; defpred S2[ Point of (TOP-REAL 2)] means $1 `2 = ((p1 `2) + (p2 `2)) / 2; reconsider Q2 = { H1(q) where q is Point of (TOP-REAL 2) : S2[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8(); A5: y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q2) by Def2; A6: P meets Q2 by A1, Th14; P /\ Q2 is closed by A1, Th14; then y_Middle (P,p1,p2) in P /\ Q2 by A1, A5, A6, JORDAN5C:def_1; hence ( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P ) by A4, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: JORDAN6:16 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 ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) 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 ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) A2: now__::_thesis:_(_p1_=_x_Middle_(P,p1,p2)_implies_p1_`1_=_p2_`1_) assume A3: p1 = x_Middle (P,p1,p2) ; ::_thesis: p1 `1 = p2 `1 deffunc H1( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1; defpred S1[ Point of (TOP-REAL 2)] means $1 `1 = ((p1 `1) + (p2 `1)) / 2; reconsider Q1 = { H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8(); A4: P meets Q1 by A1, Th13; A5: P /\ Q1 is closed by A1, Th13; x_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def1; then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def_1; then p1 in Q1 by XBOOLE_0:def_4; then ex q being Point of (TOP-REAL 2) st ( q = p1 & q `1 = ((p1 `1) + (p2 `1)) / 2 ) ; hence p1 `1 = p2 `1 ; ::_thesis: verum end; now__::_thesis:_(_p1_`1_=_p2_`1_implies_p1_=_x_Middle_(P,p1,p2)_) assume A6: p1 `1 = p2 `1 ; ::_thesis: p1 = x_Middle (P,p1,p2) for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds p1 = First_Point (P,p1,p2,Q) proof let Q be Subset of (TOP-REAL 2); ::_thesis: ( Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } implies p1 = First_Point (P,p1,p2,Q) ) assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } ; ::_thesis: p1 = First_Point (P,p1,p2,Q) then A8: p1 in Q by A6; P /\ Q is closed by A1, A7, Th13; hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; ::_thesis: verum end; hence p1 = x_Middle (P,p1,p2) by Def1; ::_thesis: verum end; hence ( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 ) by A2; ::_thesis: verum end; theorem :: JORDAN6:17 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 ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) 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 ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) A2: now__::_thesis:_(_p1_=_y_Middle_(P,p1,p2)_implies_p1_`2_=_p2_`2_) assume A3: p1 = y_Middle (P,p1,p2) ; ::_thesis: p1 `2 = p2 `2 deffunc H1( Point of (TOP-REAL 2)) -> Point of (TOP-REAL 2) = $1; defpred S1[ Point of (TOP-REAL 2)] means $1 `2 = ((p1 `2) + (p2 `2)) / 2; reconsider Q1 = { H1(q) where q is Point of (TOP-REAL 2) : S1[q] } as Subset of (TOP-REAL 2) from DOMAIN_1:sch_8(); A4: P meets Q1 by A1, Th14; A5: P /\ Q1 is closed by A1, Th14; y_Middle (P,p1,p2) = First_Point (P,p1,p2,Q1) by Def2; then p1 in P /\ Q1 by A1, A3, A4, A5, JORDAN5C:def_1; then p1 in Q1 by XBOOLE_0:def_4; then ex q being Point of (TOP-REAL 2) st ( q = p1 & q `2 = ((p1 `2) + (p2 `2)) / 2 ) ; hence p1 `2 = p2 `2 ; ::_thesis: verum end; now__::_thesis:_(_p1_`2_=_p2_`2_implies_p1_=_y_Middle_(P,p1,p2)_) assume A6: p1 `2 = p2 `2 ; ::_thesis: p1 = y_Middle (P,p1,p2) for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds p1 = First_Point (P,p1,p2,Q) proof let Q be Subset of (TOP-REAL 2); ::_thesis: ( Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } implies p1 = First_Point (P,p1,p2,Q) ) assume A7: Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } ; ::_thesis: p1 = First_Point (P,p1,p2,Q) then A8: p1 in Q by A6; P /\ Q is closed by A1, A7, Th14; hence p1 = First_Point (P,p1,p2,Q) by A1, A8, JORDAN5C:3; ::_thesis: verum end; hence p1 = y_Middle (P,p1,p2) by Def2; ::_thesis: verum end; hence ( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 ) by A2; ::_thesis: verum end; begin theorem Th18: :: JORDAN6:18 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 holds LE q2,q1,P,p2,p1 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 holds LE q2,q1,P,p2,p1 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 implies LE q2,q1,P,p2,p1 ) assume that A1: P is_an_arc_of p1,p2 and A2: LE q1,q2,P,p1,p2 ; ::_thesis: LE q2,q1,P,p2,p1 thus ( q2 in P & q1 in P ) by A2, JORDAN5C:def_3; :: according to JORDAN5C:def_3 ::_thesis: for b1 being Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) for b2, b3 being Element of REAL holds ( not b1 is being_homeomorphism or not b1 . 0 = p2 or not b1 . 1 = p1 or not b1 . b2 = q2 or not 0 <= b2 or not b2 <= 1 or not b1 . b3 = q1 or not 0 <= b3 or not b3 <= 1 or b2 <= b3 ) reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1; let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for b1, b2 being Element of REAL holds ( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . b1 = q2 or not 0 <= b1 or not b1 <= 1 or not f . b2 = q1 or not 0 <= b2 or not b2 <= 1 or b1 <= b2 ) let s1, s2 be Real; ::_thesis: ( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . s1 = q2 or not 0 <= s1 or not s1 <= 1 or not f . s2 = q1 or not 0 <= s2 or not s2 <= 1 or s1 <= s2 ) assume that A3: f is being_homeomorphism and A4: f . 0 = p2 and A5: f . 1 = p1 and A6: f . s1 = q2 and A7: 0 <= s1 and A8: s1 <= 1 and A9: f . s2 = q1 and A10: 0 <= s2 and A11: s2 <= 1 ; ::_thesis: s1 <= s2 A12: 1 - 0 >= 1 - s1 by A7, XREAL_1:13; A13: 1 - 0 >= 1 - s2 by A10, XREAL_1:13; A14: 1 - 1 <= 1 - s1 by A8, XREAL_1:13; A15: 1 - 1 <= 1 - s2 by A11, XREAL_1:13; set Ex = L[01] (((0,1) (#)),((#) (0,1))); A16: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18; set g = f * (L[01] (((0,1) (#)),((#) (0,1)))); A17: (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9; A18: (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9; dom f = [#] I[01] by A3, TOPS_2:def_5; then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A16, 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 A19: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A16, TOPMETR:20, TOPS_2:def_5; reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P9) by TOPMETR:20; A20: g is being_homeomorphism by A3, A16, TOPMETR:20, TOPS_2:57; A21: 1 - s1 in dom g by A12, A14, A19, BORSUK_1:43; A22: 1 - s2 in dom g by A13, A15, A19, BORSUK_1:43; A23: g . 0 = p1 by A5, A18, A19, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5; A24: g . 1 = p2 by A4, A17, A19, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5; reconsider qs1 = 1 - s1, qs2 = 1 - s2 as Point of (Closed-Interval-TSpace (0,1)) by A12, A13, A14, A15, BORSUK_1:43, TOPMETR:20; A25: (L[01] (((0,1) (#)),((#) (0,1)))) . qs1 = ((1 - (1 - s1)) * 1) + ((1 - s1) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3 .= s1 ; A26: (L[01] (((0,1) (#)),((#) (0,1)))) . qs2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3 .= s2 ; A27: g . (1 - s1) = q2 by A6, A21, A25, FUNCT_1:12; g . (1 - s2) = q1 by A9, A22, A26, FUNCT_1:12; then 1 - s2 <= 1 - s1 by A2, A12, A13, A14, A20, A23, A24, A27, JORDAN5C:def_3; then s1 <= 1 - (1 - s2) by XREAL_1:11; hence s1 <= s2 ; ::_thesis: verum end; definition let P be Subset of (TOP-REAL 2); let p1, p2, q1 be Point of (TOP-REAL 2); func L_Segment (P,p1,p2,q1) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 3 { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ; coherence { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2) proof { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } or x in the carrier of (TOP-REAL 2) ) assume x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q being Point of (TOP-REAL 2) st ( q = x & LE q,q1,P,p1,p2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; end; :: deftheorem defines L_Segment JORDAN6:def_3_:_ for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ; definition let P be Subset of (TOP-REAL 2); let p1, p2, q1 be Point of (TOP-REAL 2); func R_Segment (P,p1,p2,q1) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 4 { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; coherence { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2) proof { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } or x in the carrier of (TOP-REAL 2) ) assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex q being Point of (TOP-REAL 2) st ( q = x & LE q1,q,P,p1,p2 ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; end; :: deftheorem defines R_Segment JORDAN6:def_4_:_ for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; theorem Th19: :: JORDAN6:19 for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: L_Segment (P,p1,p2,q1) c= P let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L_Segment (P,p1,p2,q1) or x in P ) assume x in L_Segment (P,p1,p2,q1) ; ::_thesis: x in P then ex q being Point of (TOP-REAL 2) st ( q = x & LE q,q1,P,p1,p2 ) ; hence x in P by JORDAN5C:def_3; ::_thesis: verum end; theorem Th20: :: JORDAN6:20 for P being Subset of (TOP-REAL 2) for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: R_Segment (P,p1,p2,q1) c= P let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R_Segment (P,p1,p2,q1) or x in P ) assume x in R_Segment (P,p1,p2,q1) ; ::_thesis: x in P then ex q being Point of (TOP-REAL 2) st ( q = x & LE q1,q,P,p1,p2 ) ; hence x in P by JORDAN5C:def_3; ::_thesis: verum end; theorem :: JORDAN6:21 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 L_Segment (P,p1,p2,p1) = {p1} 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 L_Segment (P,p1,p2,p1) = {p1} let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p1) = {p1} ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: L_Segment (P,p1,p2,p1) = {p1} then A2: p1 in P by TOPREAL1:1; thus L_Segment (P,p1,p2,p1) c= {p1} :: according to XBOOLE_0:def_10 ::_thesis: {p1} c= L_Segment (P,p1,p2,p1) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L_Segment (P,p1,p2,p1) or x in {p1} ) assume x in L_Segment (P,p1,p2,p1) ; ::_thesis: x in {p1} then consider q being Point of (TOP-REAL 2) such that A3: q = x and A4: LE q,p1,P,p1,p2 ; q in P by A4, JORDAN5C:def_3; then LE p1,q,P,p1,p2 by A1, JORDAN5C:10; then q = p1 by A1, A4, JORDAN5C:12; hence x in {p1} by A3, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1} or x in L_Segment (P,p1,p2,p1) ) assume x in {p1} ; ::_thesis: x in L_Segment (P,p1,p2,p1) then A5: x = p1 by TARSKI:def_1; LE p1,p1,P,p1,p2 by A2, JORDAN5C:9; hence x in L_Segment (P,p1,p2,p1) by A5; ::_thesis: verum end; theorem :: JORDAN6:22 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 L_Segment (P,p1,p2,p2) = P 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 L_Segment (P,p1,p2,p2) = P let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,p2) = P ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: L_Segment (P,p1,p2,p2) = P thus L_Segment (P,p1,p2,p2) c= P by Th19; :: according to XBOOLE_0:def_10 ::_thesis: P c= L_Segment (P,p1,p2,p2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in L_Segment (P,p1,p2,p2) ) assume A2: x in P ; ::_thesis: x in L_Segment (P,p1,p2,p2) then reconsider p = x as Point of (TOP-REAL 2) ; LE p,p2,P,p1,p2 by A1, A2, JORDAN5C:10; hence x in L_Segment (P,p1,p2,p2) ; ::_thesis: verum end; theorem :: JORDAN6:23 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 R_Segment (P,p1,p2,p2) = {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 R_Segment (P,p1,p2,p2) = {p2} let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,p2) = {p2} ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: R_Segment (P,p1,p2,p2) = {p2} then A2: p2 in P by TOPREAL1:1; thus R_Segment (P,p1,p2,p2) c= {p2} :: according to XBOOLE_0:def_10 ::_thesis: {p2} c= R_Segment (P,p1,p2,p2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R_Segment (P,p1,p2,p2) or x in {p2} ) assume x in R_Segment (P,p1,p2,p2) ; ::_thesis: x in {p2} then consider q being Point of (TOP-REAL 2) such that A3: q = x and A4: LE p2,q,P,p1,p2 ; q in P by A4, JORDAN5C:def_3; then LE q,p2,P,p1,p2 by A1, JORDAN5C:10; then q = p2 by A1, A4, JORDAN5C:12; hence x in {p2} by A3, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p2} or x in R_Segment (P,p1,p2,p2) ) assume x in {p2} ; ::_thesis: x in R_Segment (P,p1,p2,p2) then A5: x = p2 by TARSKI:def_1; LE p2,p2,P,p1,p2 by A2, JORDAN5C:9; hence x in R_Segment (P,p1,p2,p2) by A5; ::_thesis: verum end; theorem :: JORDAN6:24 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 R_Segment (P,p1,p2,p1) = P 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 R_Segment (P,p1,p2,p1) = P let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,p1) = P ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: R_Segment (P,p1,p2,p1) = P thus R_Segment (P,p1,p2,p1) c= P by Th20; :: according to XBOOLE_0:def_10 ::_thesis: P c= R_Segment (P,p1,p2,p1) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in R_Segment (P,p1,p2,p1) ) assume A2: x in P ; ::_thesis: x in R_Segment (P,p1,p2,p1) then reconsider p = x as Point of (TOP-REAL 2) ; LE p1,p,P,p1,p2 by A1, A2, JORDAN5C:10; hence x in R_Segment (P,p1,p2,p1) ; ::_thesis: verum end; theorem :: JORDAN6:25 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 holds R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) 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 holds R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) A2: { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } c= { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } or x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } ) assume x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ; ::_thesis: x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } then consider q being Point of (TOP-REAL 2) such that A3: q = x and A4: LE q1,q,P,p1,p2 ; LE q,q1,P,p2,p1 by A1, A4, Th18; hence x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } by A3; ::_thesis: verum end; { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } c= { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q2 where q2 is Point of (TOP-REAL 2) : LE q2,q1,P,p2,p1 } or x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ) assume x in { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p2,p1 } ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } then consider q being Point of (TOP-REAL 2) such that A5: q = x and A6: LE q,q1,P,p2,p1 ; LE q1,q,P,p1,p2 by A1, A6, Th18, JORDAN5B:14; hence x in { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } by A5; ::_thesis: verum end; hence R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1) by A2, XBOOLE_0:def_10; ::_thesis: verum end; definition let P be Subset of (TOP-REAL 2); let p1, p2, q1, q2 be Point of (TOP-REAL 2); func Segment (P,p1,p2,q1,q2) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 5 (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)); correctness coherence (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Subset of (TOP-REAL 2); ; end; :: deftheorem defines Segment JORDAN6:def_5_:_ for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)); theorem :: JORDAN6:26 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,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) holds Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } thus Segment (P,p1,p2,q1,q2) c= { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } c= Segment (P,p1,p2,q1,q2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Segment (P,p1,p2,q1,q2) or x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } ) assume A1: x in Segment (P,p1,p2,q1,q2) ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } then A2: x in R_Segment (P,p1,p2,q1) by XBOOLE_0:def_4; A3: x in L_Segment (P,p1,p2,q2) by A1, XBOOLE_0:def_4; A4: ex q being Point of (TOP-REAL 2) st ( q = x & LE q1,q,P,p1,p2 ) by A2; ex p being Point of (TOP-REAL 2) st ( p = x & LE p,q2,P,p1,p2 ) by A3; hence x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } by A4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } or x in Segment (P,p1,p2,q1,q2) ) assume x in { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) } ; ::_thesis: x in Segment (P,p1,p2,q1,q2) then A5: ex q being Point of (TOP-REAL 2) st ( q = x & LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) ; then A6: x in R_Segment (P,p1,p2,q1) ; x in L_Segment (P,p1,p2,q2) by A5; hence x in Segment (P,p1,p2,q1,q2) by A6, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: JORDAN6:27 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 q2,q1,P,p2,p1 holds LE q1,q2,P,p1,p2 by Th18, JORDAN5B:14; theorem Th28: :: JORDAN6:28 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q) proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q) let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q) thus L_Segment (P,p1,p2,q) c= R_Segment (P,p2,p1,q) :: according to XBOOLE_0:def_10 ::_thesis: R_Segment (P,p2,p1,q) c= L_Segment (P,p1,p2,q) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L_Segment (P,p1,p2,q) or x in R_Segment (P,p2,p1,q) ) assume x in L_Segment (P,p1,p2,q) ; ::_thesis: x in R_Segment (P,p2,p1,q) then consider p being Point of (TOP-REAL 2) such that A2: p = x and A3: LE p,q,P,p1,p2 ; LE q,p,P,p2,p1 by A1, A3, Th18; hence x in R_Segment (P,p2,p1,q) by A2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R_Segment (P,p2,p1,q) or x in L_Segment (P,p1,p2,q) ) assume x in R_Segment (P,p2,p1,q) ; ::_thesis: x in L_Segment (P,p1,p2,q) then consider p being Point of (TOP-REAL 2) such that A4: p = x and A5: LE q,p,P,p2,p1 ; LE p,q,P,p1,p2 by A1, A5, Th18, JORDAN5B:14; hence x in L_Segment (P,p1,p2,q) by A4; ::_thesis: verum end; theorem :: JORDAN6:29 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 holds Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) 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 holds Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) ) assume A1: P is_an_arc_of p1,p2 ; ::_thesis: Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) then L_Segment (P,p1,p2,q2) = R_Segment (P,p2,p1,q2) by Th28; hence Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1) by A1, Th28, JORDAN5B:14; ::_thesis: verum end; begin definition let s be real number ; func Vertical_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 6 { p where p is Point of (TOP-REAL 2) : p `1 = s } ; correctness coherence { p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2); proof { p where p is Point of (TOP-REAL 2) : p `1 = s } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `1 = s } or x in the carrier of (TOP-REAL 2) ) assume x in { p where p is Point of (TOP-REAL 2) : p `1 = s } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex p being Point of (TOP-REAL 2) st ( p = x & p `1 = s ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; func Horizontal_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 7 { p where p is Point of (TOP-REAL 2) : p `2 = s } ; correctness coherence { p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2); proof { p where p is Point of (TOP-REAL 2) : p `2 = s } c= the carrier of (TOP-REAL 2) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of (TOP-REAL 2) : p `2 = s } or x in the carrier of (TOP-REAL 2) ) assume x in { p where p is Point of (TOP-REAL 2) : p `2 = s } ; ::_thesis: x in the carrier of (TOP-REAL 2) then ex p being Point of (TOP-REAL 2) st ( p = x & p `2 = s ) ; hence x in the carrier of (TOP-REAL 2) ; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2) ; ::_thesis: verum end; end; :: deftheorem defines Vertical_Line JORDAN6:def_6_:_ for s being real number holds Vertical_Line s = { p where p is Point of (TOP-REAL 2) : p `1 = s } ; :: deftheorem defines Horizontal_Line JORDAN6:def_7_:_ for s being real number holds Horizontal_Line s = { p where p is Point of (TOP-REAL 2) : p `2 = s } ; theorem :: JORDAN6:30 for r being real number holds ( Vertical_Line r is closed & Horizontal_Line r is closed ) by Th6, Th9; theorem Th31: :: JORDAN6:31 for r being real number for p being Point of (TOP-REAL 2) holds ( p in Vertical_Line r iff p `1 = r ) proof let r be real number ; ::_thesis: for p being Point of (TOP-REAL 2) holds ( p in Vertical_Line r iff p `1 = r ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in Vertical_Line r iff p `1 = r ) hereby ::_thesis: ( p `1 = r implies p in Vertical_Line r ) assume p in Vertical_Line r ; ::_thesis: p `1 = r then ex q being Point of (TOP-REAL 2) st ( q = p & q `1 = r ) ; hence p `1 = r ; ::_thesis: verum end; assume p `1 = r ; ::_thesis: p in Vertical_Line r hence p in Vertical_Line r ; ::_thesis: verum end; theorem :: JORDAN6:32 for r being real number for p being Point of (TOP-REAL 2) holds ( p in Horizontal_Line r iff p `2 = r ) proof let r be real number ; ::_thesis: for p being Point of (TOP-REAL 2) holds ( p in Horizontal_Line r iff p `2 = r ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in Horizontal_Line r iff p `2 = r ) hereby ::_thesis: ( p `2 = r implies p in Horizontal_Line r ) assume p in Horizontal_Line r ; ::_thesis: p `2 = r then ex q being Point of (TOP-REAL 2) st ( q = p & q `2 = r ) ; hence p `2 = r ; ::_thesis: verum end; assume p `2 = r ; ::_thesis: p in Horizontal_Line r hence p in Horizontal_Line r ; ::_thesis: verum end; theorem Th33: :: JORDAN6:33 for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) assume P is being_simple_closed_curve ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) then reconsider P = P as Simple_closed_curve ; A1: W-min P in P by SPRECT_1:13; A2: E-max P in P by SPRECT_1:14; W-min P <> E-max P by TOPREAL5:19; then consider P01, P02 being non empty Subset of (TOP-REAL 2) such that A3: P01 is_an_arc_of W-min P, E-max P and A4: P02 is_an_arc_of W-min P, E-max P and A5: P = P01 \/ P02 and A6: P01 /\ P02 = {(W-min P),(E-max P)} by A1, A2, TOPREAL2:5; reconsider P01 = P01, P02 = P02 as non empty Subset of (TOP-REAL 2) ; A7: P01 is_an_arc_of E-max P, W-min P by A3, JORDAN5B:14; A8: P02 is_an_arc_of E-max P, W-min P by A4, JORDAN5B:14; reconsider P001 = P01, P002 = P02 as non empty Subset of (TOP-REAL 2) ; A9: (E-max P) `1 = E-bound P by EUCLID:52; A10: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6; P01 is closed by A3, COMPTS_1:7, JORDAN5A:1; then A11: P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A10, TOPS_1:8; A12: Vertical_Line (((W-bound P) + (E-bound P)) / 2) is closed by Th6; P02 is closed by A4, COMPTS_1:7, JORDAN5A:1; then A13: P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, TOPS_1:8; consider q1 being Point of (TOP-REAL 2) such that A14: q1 in P001 and A15: q1 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A3, Th12; A16: (W-min P) `1 = W-bound P by EUCLID:52; (E-max P) `1 = E-bound P by EUCLID:52; then q1 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A15, A16; then P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A14, XBOOLE_0:def_4; then A17: P01 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by XBOOLE_0:def_7; consider q2 being Point of (TOP-REAL 2) such that A18: q2 in P002 and A19: q2 `1 = (((W-min P) `1) + ((E-max P) `1)) / 2 by A4, Th12; q2 in { p where p is Point of (TOP-REAL 2) : p `1 = ((W-bound P) + (E-bound P)) / 2 } by A9, A16, A19; then P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) <> {} by A18, XBOOLE_0:def_4; then A20: P02 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by XBOOLE_0:def_7; percases ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 or (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 <= (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ; suppose (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A3, A5, A6, A8; ::_thesis: verum end; supposeA21: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 <= (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) now__::_thesis:_(_(_(First_Point_(P01,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_<_(Last_Point_(P02,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_&_ex_P1,_P2_being_non_empty_Subset_of_(TOP-REAL_2)_st_ (_P1_is_an_arc_of_W-min_P,_E-max_P_&_P2_is_an_arc_of_E-max_P,_W-min_P_&_P1_/\_P2_=_{(W-min_P),(E-max_P)}_&_P1_\/_P2_=_P_&_(First_Point_(P1,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_>_(Last_Point_(P2,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_)_)_or_(_(First_Point_(P01,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_=_(Last_Point_(P02,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_&_contradiction_)_) percases ( (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 or (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A21, XXREAL_0:1; caseA22: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 < (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) A23: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P01,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A3, A11, A17, JORDAN5C:18; Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = First_Point (P02,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A4, A13, A20, JORDAN5C:18; hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A4, A5, A6, A7, A22, A23; ::_thesis: verum end; caseA24: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 = (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: contradiction set p = First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))); set p9 = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))); A25: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A3, A11, A17, JORDAN5C:def_1; then A26: First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 by XBOOLE_0:def_4; First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A25, XBOOLE_0:def_4; then A27: (First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31; A28: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) by A8, A13, A20, JORDAN5C:def_2; then A29: Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P02 by XBOOLE_0:def_4; Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A28, XBOOLE_0:def_4; then (Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `1 = ((W-bound P) + (E-bound P)) / 2 by Th31; then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = Last_Point (P02,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) by A24, A27, TOPREAL3:6; then First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) in P01 /\ P02 by A26, A29, XBOOLE_0:def_4; then ( First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = W-min P or First_Point (P01,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) = E-max P ) by A6, TARSKI:def_2; hence contradiction by A9, A16, A27, TOPREAL5:17; ::_thesis: verum end; end; end; then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that A30: P1 is_an_arc_of W-min P, E-max P and A31: P2 is_an_arc_of E-max P, W-min P and A32: P1 /\ P2 = {(W-min P),(E-max P)} and A33: P1 \/ P2 = P and A34: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ; take P1 ; ::_thesis: ex P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) take P2 ; ::_thesis: ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) thus ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A30, A31, A32, A33, A34; ::_thesis: verum end; end; end; begin theorem Th34: :: JORDAN6:34 for P being Subset of I[01] st P = the carrier of I[01] \ {0,1} holds P is open proof let P be Subset of I[01]; ::_thesis: ( P = the carrier of I[01] \ {0,1} implies P is open ) assume A1: P = the carrier of I[01] \ {0,1} ; ::_thesis: P is open A2: 0 in [.0,1.] by XXREAL_1:1; A3: 1 in [.0,1.] by XXREAL_1:1; reconsider Q0 = {0} as Subset of I[01] by A2, BORSUK_1:40, ZFMISC_1:31; reconsider Q1 = {1} as Subset of I[01] by A3, BORSUK_1:40, ZFMISC_1:31; Q0 \/ Q1 is closed by A2, A3, BORSUK_1:40, TOPS_1:9; then ([#] I[01]) \ (Q0 \/ Q1) is open by PRE_TOPC:def_3; hence P is open by A1, ENUMSET1:1; ::_thesis: verum end; theorem :: JORDAN6:35 for P being Subset of R^1 for r, s being real number st P = ].r,s.[ holds P is open proof let P be Subset of R^1; ::_thesis: for r, s being real number st P = ].r,s.[ holds P is open let r, s be real number ; ::_thesis: ( P = ].r,s.[ implies P is open ) assume A1: P = ].r,s.[ ; ::_thesis: P is open { r1 where r1 is Real : r < r1 } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r1 where r1 is Real : r < r1 } or x in REAL ) assume x in { r1 where r1 is Real : r < r1 } ; ::_thesis: x in REAL then ex r1 being Real st ( r1 = x & r < r1 ) ; hence x in REAL ; ::_thesis: verum end; then reconsider P1 = { r1 where r1 is Real : r < r1 } as Subset of R^1 by TOPMETR:17; { r2 where r2 is Real : s > r2 } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r2 where r2 is Real : s > r2 } or x in REAL ) assume x in { r2 where r2 is Real : s > r2 } ; ::_thesis: x in REAL then ex r2 being Real st ( r2 = x & s > r2 ) ; hence x in REAL ; ::_thesis: verum end; then reconsider P2 = { r2 where r2 is Real : s > r2 } as Subset of R^1 by TOPMETR:17; A2: P1 is open by JORDAN2B:25; A3: P2 is open by JORDAN2B:24; A4: P c= P1 /\ P2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in P1 /\ P2 ) assume A5: x in P ; ::_thesis: x in P1 /\ P2 then reconsider r1 = x as Real by TOPMETR:17; A6: r < r1 by A1, A5, XXREAL_1:4; A7: r1 < s by A1, A5, XXREAL_1:4; A8: x in P1 by A6; x in P2 by A7; hence x in P1 /\ P2 by A8, XBOOLE_0:def_4; ::_thesis: verum end; P1 /\ P2 c= P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 /\ P2 or x in P ) assume A9: x in P1 /\ P2 ; ::_thesis: x in P then A10: x in P1 by XBOOLE_0:def_4; A11: x in P2 by A9, XBOOLE_0:def_4; A12: ex r1 being Real st ( r1 = x & r < r1 ) by A10; ex r2 being Real st ( r2 = x & s > r2 ) by A11; hence x in P by A1, A12, XXREAL_1:4; ::_thesis: verum end; then P = P1 /\ P2 by A4, XBOOLE_0:def_10; hence P is open by A2, A3, TOPS_1:11; ::_thesis: verum end; theorem Th36: :: JORDAN6:36 for P7 being Subset of I[01] st P7 = the carrier of I[01] \ {0,1} holds ( P7 <> {} & P7 is connected ) proof let P7 be Subset of I[01]; ::_thesis: ( P7 = the carrier of I[01] \ {0,1} implies ( P7 <> {} & P7 is connected ) ) assume A1: P7 = the carrier of I[01] \ {0,1} ; ::_thesis: ( P7 <> {} & P7 is connected ) A2: 1 / 2 in [.0,1.] by XXREAL_1:1; A3: not 1 / 2 in {0,1} by TARSKI:def_2; A4: [#] (I[01] | P7) = P7 by PRE_TOPC:def_5; for A, B being Subset of (I[01] | P7) st [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open holds A meets B proof let A, B be Subset of (I[01] | P7); ::_thesis: ( [#] (I[01] | P7) = A \/ B & A <> {} (I[01] | P7) & B <> {} (I[01] | P7) & A is open & B is open implies A meets B ) assume that A5: [#] (I[01] | P7) = A \/ B and A6: A <> {} (I[01] | P7) and A7: B <> {} (I[01] | P7) and A8: A is open and A9: B is open ; ::_thesis: A meets B assume A10: A misses B ; ::_thesis: contradiction A11: ].0,1.[ misses {0,1} by XXREAL_1:86; A12: P7 = (].0,1.[ \/ {0,1}) \ {0,1} by A1, BORSUK_1:40, XXREAL_1:128 .= ].0,1.[ \ {0,1} by XBOOLE_1:40 .= ].0,1.[ by A11, XBOOLE_1:83 ; reconsider D1 = [.0,1.] as Subset of R^1 by TOPMETR:17; reconsider P1 = P7 as Subset of R^1 by A12, TOPMETR:17; I[01] = R^1 | D1 by TOPMETR:19, TOPMETR:20; then A13: I[01] | P7 = R^1 | P1 by BORSUK_1:40, PRE_TOPC:7; P1 = { r1 where r1 is Real : ( 0 < r1 & r1 < 1 ) } by A12, RCOMP_1:def_2; then P1 is open by JORDAN2B:26; then A14: I[01] | P7 is non empty open SubSpace of R^1 by A1, A2, A3, A4, A13, BORSUK_1:40, TSEP_1:16, XBOOLE_0:def_5; reconsider P = A, Q = B as non empty Subset of REAL by A4, A6, A7, A12, XBOOLE_1:1; reconsider A0 = P, B0 = Q as non empty Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; A15: A0 is open by A8, A14, TSEP_1:17; A16: B0 is open by A9, A14, TSEP_1:17; set xp = the Element of P; reconsider xp = the Element of P as Real ; A17: xp in P ; 0 is LowerBound of P proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in P or 0 <= r ) assume r in P ; ::_thesis: 0 <= r then r in ].0,1.[ by A4, A12; then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def_2; then ex u being Real st ( u = r & 0 < u & u < 1 ) ; hence 0 <= r ; ::_thesis: verum end; then A18: P is bounded_below by XXREAL_2:def_9; 0 is LowerBound of Q proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Q or 0 <= r ) assume r in Q ; ::_thesis: 0 <= r then r in ].0,1.[ by A4, A12; then r in { w where w is Real : ( 0 < w & w < 1 ) } by RCOMP_1:def_2; then ex u being Real st ( u = r & 0 < u & u < 1 ) ; hence 0 <= r ; ::_thesis: verum end; then A19: Q is bounded_below by XXREAL_2:def_9; reconsider l = lower_bound Q as Element of REAL ; reconsider m = l as Point of RealSpace by METRIC_1:def_13; reconsider t = m as Point of R^1 by TOPMETR:12, TOPMETR:def_6; A20: not l in Q proof assume l in Q ; ::_thesis: contradiction then consider s being real number such that A21: s > 0 and A22: Ball (m,s) c= B0 by A16, TOPMETR:15, TOPMETR:def_6; reconsider s = s as Element of REAL by XREAL_0:def_1; reconsider e1 = l - (s / 2) as Point of RealSpace by METRIC_1:def_13; s / 2 < s by A21, XREAL_1:216; then abs (l - (l - (s / 2))) < s by A21, ABSVALUE:def_1; then the distance of RealSpace . (m,e1) < s by METRIC_1:def_12, METRIC_1:def_13; then dist (m,e1) < s by METRIC_1:def_1; then e1 in { z where z is Element of RealSpace : dist (m,z) < s } ; then l - (s / 2) in Ball (m,s) by METRIC_1:17; then l <= l - (s / 2) by A19, A22, SEQ_4:def_2; then l + (s / 2) <= l by XREAL_1:19; then (l + (s / 2)) - l <= l - l by XREAL_1:9; hence contradiction by A21, XREAL_1:139; ::_thesis: verum end; A23: now__::_thesis:_not_l_<=_0 assume A24: l <= 0 ; ::_thesis: contradiction 0 < xp by A4, A12, A17, XXREAL_1:4; then consider r5 being real number such that A25: r5 in Q and A26: r5 < l + (xp - l) by A19, A24, SEQ_4:def_2; reconsider r5 = r5 as Real by XREAL_0:def_1; A27: { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } c= P proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } or y in P ) assume y in { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } ; ::_thesis: y in P then ex s5 being Real st ( s5 = y & s5 in P & r5 < s5 ) ; hence y in P ; ::_thesis: verum end; then reconsider P5 = { s5 where s5 is Real : ( s5 in P & r5 < s5 ) } as Subset of REAL by XBOOLE_1:1; A28: xp in P5 by A26; A29: P5 is bounded_below by A18, A27, XXREAL_2:44; reconsider l5 = lower_bound P5 as Real ; reconsider m5 = l5 as Point of RealSpace by METRIC_1:def_13; A30: now__::_thesis:_not_l5_<=_r5 assume A31: l5 <= r5 ; ::_thesis: contradiction now__::_thesis:_not_l5_<_r5 assume l5 < r5 ; ::_thesis: contradiction then r5 - l5 > 0 by XREAL_1:50; then consider r being real number such that A32: r in P5 and A33: r < l5 + (r5 - l5) by A28, A29, SEQ_4:def_2; ex s6 being Real st ( s6 = r & s6 in P & r5 < s6 ) by A32; hence contradiction by A33; ::_thesis: verum end; then l5 = r5 by A31, XXREAL_0:1; then consider r7 being real number such that A34: r7 > 0 and A35: Ball (m5,r7) c= B0 by A16, A25, TOPMETR:15, TOPMETR:def_6; consider r9 being real number such that A36: r9 in P5 and A37: r9 < l5 + r7 by A28, A29, A34, SEQ_4:def_2; reconsider r9 = r9 as Real by XREAL_0:def_1; reconsider e8 = r9 as Point of RealSpace by METRIC_1:def_13; l5 <= r9 by A29, A36, SEQ_4:def_2; then A38: r9 - l5 >= 0 by XREAL_1:48; r9 - l5 < (l5 + r7) - l5 by A37, XREAL_1:9; then abs (r9 - l5) < r7 by A38, ABSVALUE:def_1; then the distance of RealSpace . (e8,m5) < r7 by METRIC_1:def_12, METRIC_1:def_13; then dist (e8,m5) < r7 by METRIC_1:def_1; then e8 in { z where z is Element of RealSpace : dist (m5,z) < r7 } ; then e8 in Ball (m5,r7) by METRIC_1:17; hence contradiction by A10, A27, A35, A36, XBOOLE_0:3; ::_thesis: verum end; A39: 0 < r5 by A4, A12, A25, XXREAL_1:4; A40: l5 - r5 > 0 by A30, XREAL_1:50; set q = the Element of P5; A41: the Element of P5 in P5 by A28; then reconsider q1 = the Element of P5 as Real ; q1 in P by A27, A41; then A42: q1 < 1 by A4, A12, XXREAL_1:4; l5 <= q1 by A28, A29, SEQ_4:def_2; then l5 < 1 by A42, XXREAL_0:2; then l5 in ].0,1.[ by A30, A39, XXREAL_1:4; then A43: ( l5 in P or l5 in Q ) by A4, A5, A12, XBOOLE_0:def_3; now__::_thesis:_not_l5_in_P assume l5 in P ; ::_thesis: contradiction then consider s5 being real number such that A44: s5 > 0 and A45: Ball (m5,s5) c= P by A15, TOPMETR:15, TOPMETR:def_6; reconsider s5 = s5 as Element of REAL by XREAL_0:def_1; set s59 = min (s5,(l5 - r5)); A46: min (s5,(l5 - r5)) > 0 by A40, A44, XXREAL_0:21; A47: min (s5,(l5 - r5)) <= s5 by XXREAL_0:17; A48: (min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216; min (s5,(l5 - r5)) <= l5 - r5 by XXREAL_0:17; then (min (s5,(l5 - r5))) / 2 < l5 - r5 by A48, XXREAL_0:2; then ((min (s5,(l5 - r5))) / 2) + r5 < (l5 - r5) + r5 by XREAL_1:6; then A49: (((min (s5,(l5 - r5))) / 2) + r5) - ((min (s5,(l5 - r5))) / 2) < l5 - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9; reconsider e1 = l5 - ((min (s5,(l5 - r5))) / 2) as Point of RealSpace by METRIC_1:def_13; (min (s5,(l5 - r5))) / 2 < min (s5,(l5 - r5)) by A46, XREAL_1:216; then (min (s5,(l5 - r5))) / 2 < s5 by A47, XXREAL_0:2; then abs (l5 - (l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by A46, ABSVALUE:def_1; then real_dist . (l5,(l5 - ((min (s5,(l5 - r5))) / 2))) < s5 by METRIC_1:def_12; then dist (m5,e1) < s5 by METRIC_1:def_1, METRIC_1:def_13; then e1 in { z where z is Element of RealSpace : dist (m5,z) < s5 } ; then l5 - ((min (s5,(l5 - r5))) / 2) in Ball (m5,s5) by METRIC_1:17; then A50: l5 - ((min (s5,(l5 - r5))) / 2) in { s7 where s7 is Real : ( s7 in P & r5 < s7 ) } by A45, A49; l5 < l5 + ((min (s5,(l5 - r5))) / 2) by A46, XREAL_1:29, XREAL_1:139; then l5 - ((min (s5,(l5 - r5))) / 2) < (l5 + ((min (s5,(l5 - r5))) / 2)) - ((min (s5,(l5 - r5))) / 2) by XREAL_1:9; hence contradiction by A29, A50, SEQ_4:def_2; ::_thesis: verum end; then consider s1 being real number such that A51: s1 > 0 and A52: Ball (m5,s1) c= B0 by A16, A43, TOPMETR:15, TOPMETR:def_6; s1 / 2 > 0 by A51, XREAL_1:139; then consider r2 being real number such that A53: r2 in P5 and A54: r2 < l5 + (s1 / 2) by A28, A29, SEQ_4:def_2; reconsider r2 = r2 as Real by XREAL_0:def_1; A55: l5 <= r2 by A29, A53, SEQ_4:def_2; reconsider s3 = r2 - l5 as Real ; reconsider e1 = l5 + s3 as Point of RealSpace by METRIC_1:def_13; A56: r2 - l5 >= 0 by A55, XREAL_1:48; A57: r2 - l5 < (l5 + (s1 / 2)) - l5 by A54, XREAL_1:14; s1 / 2 < s1 by A51, XREAL_1:216; then A58: (l5 + s3) - l5 < s1 by A57, XXREAL_0:2; abs ((l5 + s3) - l5) = (l5 + s3) - l5 by A56, ABSVALUE:def_1; then real_dist . ((l5 + s3),l5) < s1 by A58, METRIC_1:def_12; then dist (e1,m5) < s1 by METRIC_1:def_1, METRIC_1:def_13; then l5 + s3 in { z where z is Element of RealSpace : dist (m5,z) < s1 } ; then l5 + s3 in Ball (m5,s1) by METRIC_1:17; then A59: l5 + s3 in P5 /\ Q by A52, A53, XBOOLE_0:def_4; P5 /\ Q c= P /\ Q by A27, XBOOLE_1:26; hence contradiction by A10, A59, XBOOLE_0:def_7; ::_thesis: verum end; set q = the Element of Q; A60: the Element of Q in Q ; reconsider q1 = the Element of Q as Real ; A61: q1 < 1 by A4, A12, A60, XXREAL_1:4; l <= q1 by A19, SEQ_4:def_2; then l < 1 by A61, XXREAL_0:2; then l in ].0,1.[ by A23, XXREAL_1:4; then A62: t in A0 by A4, A5, A12, A20, XBOOLE_0:def_3; A0 is open by A8, A14, TSEP_1:17; then consider s1 being real number such that A63: s1 > 0 and A64: Ball (m,s1) c= A0 by A62, TOPMETR:15, TOPMETR:def_6; s1 / 2 > 0 by A63, XREAL_1:139; then consider r2 being real number such that A65: r2 in Q and A66: r2 < l + (s1 / 2) by A19, SEQ_4:def_2; reconsider r2 = r2 as Real by XREAL_0:def_1; A67: l <= r2 by A19, A65, SEQ_4:def_2; set s3 = r2 - l; reconsider e1 = l + (r2 - l) as Point of RealSpace by METRIC_1:def_13; A68: r2 - l >= 0 by A67, XREAL_1:48; A69: r2 - l < (l + (s1 / 2)) - l by A66, XREAL_1:14; s1 / 2 < s1 by A63, XREAL_1:216; then A70: (l + (r2 - l)) - l < s1 by A69, XXREAL_0:2; abs ((l + (r2 - l)) - l) = (l + (r2 - l)) - l by A68, ABSVALUE:def_1; then real_dist . ((l + (r2 - l)),l) < s1 by A70, METRIC_1:def_12; then dist (e1,m) < s1 by METRIC_1:def_1, METRIC_1:def_13; then l + (r2 - l) in { z where z is Element of RealSpace : dist (m,z) < s1 } ; then l + (r2 - l) in Ball (m,s1) by METRIC_1:17; hence contradiction by A10, A64, A65, XBOOLE_0:3; ::_thesis: verum end; then I[01] | P7 is connected by CONNSP_1:11; hence ( P7 <> {} & P7 is connected ) by A1, A2, A3, BORSUK_1:40, CONNSP_1:def_3, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th37: :: JORDAN6:37 for n being Element of NAT for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds p1 <> p2 proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds p1 <> p2 let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds p1 <> p2 let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies p1 <> p2 ) assume P is_an_arc_of p1,p2 ; ::_thesis: p1 <> p2 then consider f being Function of I[01],((TOP-REAL n) | P) such that A1: f is being_homeomorphism and A2: f . 0 = p1 and A3: f . 1 = p2 by TOPREAL1:def_1; 1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then A4: 1 in dom f by A1, TOPS_2:def_5; A5: f is one-to-one by A1, TOPS_2:def_5; 0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then 0 in dom f by A1, TOPS_2:def_5; hence p1 <> p2 by A2, A3, A4, A5, FUNCT_1:def_4; ::_thesis: verum end; theorem :: JORDAN6:38 for n being Element of NAT for P being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is open proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is open let P be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is open let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is open let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} implies Q is open ) assume that A1: P is_an_arc_of p1,p2 and A2: Q = P \ {p1,p2} ; ::_thesis: Q is open reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1; consider f being Function of I[01],((TOP-REAL n) | P9) such that A3: f is being_homeomorphism and A4: f . 0 = p1 and A5: f . 1 = p2 by A1, TOPREAL1:def_1; reconsider f1 = f as Function ; A6: f " is being_homeomorphism by A3, TOPS_2:56; reconsider g = f " as Function of ((TOP-REAL n) | P),I[01] ; reconsider g1 = g as Function ; reconsider R = the carrier of I[01] \ {0,1} as Subset of I[01] ; A7: [#] I[01] <> {} ; A8: R is open by Th34; A9: f is one-to-one by A3, TOPS_2:def_5; A10: g is one-to-one by A6, TOPS_2:def_5; A11: g is continuous by A3, TOPS_2:def_5; A12: [#] I[01] = dom f by A3, TOPS_2:def_5; 0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then A13: 0 in dom f by A3, TOPS_2:def_5; 1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then A14: 1 in dom f by A3, TOPS_2:def_5; rng f = [#] ((TOP-REAL n) | P) by A3, TOPS_2:def_5; then A15: (f ") " = f by A9, TOPS_2:51; rng g = [#] I[01] by A6, TOPS_2:def_5; then g is onto by FUNCT_2:def_3; then A16: g1 " = f1 by A10, A15, TOPS_2:def_4; g " R = (g1 " the carrier of I[01]) \ (g1 " {0,1}) by FUNCT_1:69 .= ((g1 ") .: the carrier of I[01]) \ (g1 " {0,1}) by A10, FUNCT_1:85 .= (f1 .: ([#] I[01])) \ (f1 .: {0,1}) by A10, A16, FUNCT_1:85 .= (rng f) \ (f .: {0,1}) by A12, RELAT_1:113 .= ([#] ((TOP-REAL n) | P)) \ (f .: {0,1}) by A3, TOPS_2:def_5 .= P \ (f .: {0,1}) by PRE_TOPC:def_5 .= Q by A2, A4, A5, A13, A14, FUNCT_1:60 ; hence Q is open by A7, A8, A11, TOPS_2:43; ::_thesis: verum end; theorem Th39: :: JORDAN6:39 for n being Element of NAT for P, P1, P2 being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds Q is open proof let n be Element of NAT ; ::_thesis: for P, P1, P2 being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds Q is open let P, P1, P2 be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds Q is open let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds Q is open let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} implies Q is open ) assume that A1: P2 is_an_arc_of p1,p2 and A2: P1 \/ P2 = P and A3: P1 /\ P2 = {p1,p2} and A4: Q = P1 \ {p1,p2} ; ::_thesis: Q is open reconsider P21 = P2 as Subset of (TOP-REAL n) ; A5: P21 is compact by A1, JORDAN5A:1; p1 in P1 /\ P2 by A3, TARSKI:def_2; then A6: p1 in P2 by XBOOLE_0:def_4; A7: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def_5; then reconsider P29 = P21 as Subset of ((TOP-REAL n) | P) by A2, XBOOLE_1:7; p2 in P1 /\ P2 by A3, TARSKI:def_2; then A8: p2 in P2 by XBOOLE_0:def_4; P29 is compact by A5, A7, COMPTS_1:2; then A9: P29 is closed by COMPTS_1:7; A10: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by A2, XBOOLE_1:42 .= (P1 \ P2) \/ {} by XBOOLE_1:37 .= P1 \ P2 ; A11: P1 \ P2 c= Q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 \ P2 or x in Q ) assume A12: x in P1 \ P2 ; ::_thesis: x in Q then A13: x in P1 by XBOOLE_0:def_5; not x in P2 by A12, XBOOLE_0:def_5; then not x in {p1,p2} by A6, A8, TARSKI:def_2; hence x in Q by A4, A13, XBOOLE_0:def_5; ::_thesis: verum end; Q c= P1 \ P2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in P1 \ P2 ) assume A14: x in Q ; ::_thesis: x in P1 \ P2 then A15: x in P1 by A4, XBOOLE_0:def_5; not x in {p1,p2} by A4, A14, XBOOLE_0:def_5; then not x in P2 by A3, A15, XBOOLE_0:def_4; hence x in P1 \ P2 by A15, XBOOLE_0:def_5; ::_thesis: verum end; then P1 \ P2 = Q by A11, XBOOLE_0:def_10; then Q = P29 ` by A7, A10, SUBSET_1:def_4; hence Q is open by A9, TOPS_1:3; ::_thesis: verum end; theorem Th40: :: JORDAN6:40 for n being Element of NAT for P being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is connected proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is connected let P be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is connected let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds Q is connected let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & Q = P \ {p1,p2} implies Q is connected ) assume that A1: P is_an_arc_of p1,p2 and A2: Q = P \ {p1,p2} ; ::_thesis: Q is connected reconsider P9 = P as non empty Subset of (TOP-REAL n) by A1, TOPREAL1:1; consider f being Function of I[01],((TOP-REAL n) | P9) such that A3: f is being_homeomorphism and A4: f . 0 = p1 and A5: f . 1 = p2 by A1, TOPREAL1:def_1; reconsider P7 = the carrier of I[01] \ {0,1} as Subset of I[01] ; A6: f is continuous by A3, TOPS_2:def_5; A7: f is one-to-one by A3, TOPS_2:def_5; Q = f .: P7 proof [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def_5; then A8: rng f = P by A3, TOPS_2:def_5; thus Q c= f .: P7 :: according to XBOOLE_0:def_10 ::_thesis: f .: P7 c= Q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in f .: P7 ) assume A9: x in Q ; ::_thesis: x in f .: P7 then A10: x in P by A2, XBOOLE_0:def_5; A11: not x in {p1,p2} by A2, A9, XBOOLE_0:def_5; consider z being set such that A12: z in dom f and A13: x = f . z by A8, A10, FUNCT_1:def_3; now__::_thesis:_not_z_in_{0,1} assume z in {0,1} ; ::_thesis: contradiction then ( x = p1 or x = p2 ) by A4, A5, A13, TARSKI:def_2; hence contradiction by A11, TARSKI:def_2; ::_thesis: verum end; then z in P7 by A12, XBOOLE_0:def_5; hence x in f .: P7 by A12, A13, FUNCT_1:def_6; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: P7 or y in Q ) assume y in f .: P7 ; ::_thesis: y in Q then consider x being set such that A14: x in dom f and A15: x in P7 and A16: y = f . x by FUNCT_1:def_6; A17: not x in {0,1} by A15, XBOOLE_0:def_5; then A18: x <> 0 by TARSKI:def_2; A19: x <> 1 by A17, TARSKI:def_2; A20: y in P by A8, A14, A16, FUNCT_1:def_3; now__::_thesis:_not_y_in_{p1,p2} assume A21: y in {p1,p2} ; ::_thesis: contradiction reconsider f1 = f as Function of the carrier of I[01], the carrier of ((TOP-REAL n) | P9) ; now__::_thesis:_(_(_f_._x_=_p1_&_contradiction_)_or_(_f_._x_=_p2_&_contradiction_)_) percases ( f . x = p1 or f . x = p2 ) by A16, A21, TARSKI:def_2; caseA22: f . x = p1 ; ::_thesis: contradiction dom f1 = the carrier of I[01] by FUNCT_2:def_1; then 0 in dom f1 by BORSUK_1:40, XXREAL_1:1; hence contradiction by A4, A7, A14, A18, A22, FUNCT_1:def_4; ::_thesis: verum end; caseA23: f . x = p2 ; ::_thesis: contradiction dom f1 = the carrier of I[01] by FUNCT_2:def_1; then 1 in dom f1 by BORSUK_1:40, XXREAL_1:1; hence contradiction by A5, A7, A14, A19, A23, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence y in Q by A2, A20, XBOOLE_0:def_5; ::_thesis: verum end; hence Q is connected by A6, Th36, TOPS_2:61; ::_thesis: verum end; theorem Th41: :: JORDAN6:41 for GX being TopSpace for P1, P being Subset of GX for Q9 being Subset of (GX | P1) for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds Q is connected proof let GX be TopSpace; ::_thesis: for P1, P being Subset of GX for Q9 being Subset of (GX | P1) for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds Q is connected let P1, P be Subset of GX; ::_thesis: for Q9 being Subset of (GX | P1) for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds Q is connected let Q9 be Subset of (GX | P1); ::_thesis: for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds Q is connected let Q be Subset of (GX | P); ::_thesis: ( P1 c= P & Q = Q9 & Q9 is connected implies Q is connected ) assume that A1: P1 c= P and A2: Q = Q9 and A3: Q9 is connected ; ::_thesis: Q is connected [#] (GX | P) = P by PRE_TOPC:def_5; then reconsider P19 = P1 as Subset of (GX | P) by A1; GX | P1 = (GX | P) | P19 by A1, PRE_TOPC:7; hence Q is connected by A2, A3, CONNSP_1:23; ::_thesis: verum end; theorem Th42: :: JORDAN6:42 for n being Element of NAT for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds ex p3 being Point of (TOP-REAL n) st ( p3 in P & p3 <> p1 & p3 <> p2 ) proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds ex p3 being Point of (TOP-REAL n) st ( p3 in P & p3 <> p1 & p3 <> p2 ) let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds ex p3 being Point of (TOP-REAL n) st ( p3 in P & p3 <> p1 & p3 <> p2 ) let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies ex p3 being Point of (TOP-REAL n) st ( p3 in P & p3 <> p1 & p3 <> p2 ) ) assume P is_an_arc_of p1,p2 ; ::_thesis: ex p3 being Point of (TOP-REAL n) st ( p3 in P & p3 <> p1 & p3 <> p2 ) then consider f being Function of I[01],((TOP-REAL n) | P) such that A1: f is being_homeomorphism and A2: f . 0 = p1 and A3: f . 1 = p2 by TOPREAL1:def_1; 1 / 2 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then A4: 1 / 2 in dom f by A1, TOPS_2:def_5; then f . (1 / 2) in rng f by FUNCT_1:def_3; then f . (1 / 2) in the carrier of ((TOP-REAL n) | P) ; then A5: f . (1 / 2) in P by PRE_TOPC:8; then reconsider p = f . (1 / 2) as Point of (TOP-REAL n) ; A6: f is one-to-one by A1, TOPS_2:def_5; 0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then 0 in dom f by A1, TOPS_2:def_5; then A7: p1 <> p by A2, A4, A6, FUNCT_1:def_4; 1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1; then 1 in dom f by A1, TOPS_2:def_5; then f . 1 <> f . (1 / 2) by A4, A6, FUNCT_1:def_4; hence ex p3 being Point of (TOP-REAL n) st ( p3 in P & p3 <> p1 & p3 <> p2 ) by A3, A5, A7; ::_thesis: verum end; theorem :: JORDAN6:43 for n being Element of NAT for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P \ {p1,p2} <> {} proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P \ {p1,p2} <> {} let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds P \ {p1,p2} <> {} let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 implies P \ {p1,p2} <> {} ) assume P is_an_arc_of p1,p2 ; ::_thesis: P \ {p1,p2} <> {} then consider p3 being Point of (TOP-REAL n) such that A1: p3 in P and A2: p3 <> p1 and A3: p3 <> p2 by Th42; not p3 in {p1,p2} by A2, A3, TARSKI:def_2; hence P \ {p1,p2} <> {} by A1, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: JORDAN6:44 for n being Element of NAT for P1, P being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds Q is connected proof let n be Element of NAT ; ::_thesis: for P1, P being Subset of (TOP-REAL n) for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds Q is connected let P1, P be Subset of (TOP-REAL n); ::_thesis: for Q being Subset of ((TOP-REAL n) | P) for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds Q is connected let Q be Subset of ((TOP-REAL n) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds Q is connected let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} implies Q is connected ) assume that A1: P1 is_an_arc_of p1,p2 and A2: P1 c= P and A3: Q = P1 \ {p1,p2} ; ::_thesis: Q is connected [#] ((TOP-REAL n) | P1) = P1 by PRE_TOPC:def_5; then reconsider Q9 = Q as Subset of ((TOP-REAL n) | P1) by A3, XBOOLE_1:36; Q9 is connected by A1, A3, Th40; hence Q is connected by A2, Th41; ::_thesis: verum end; theorem Th45: :: JORDAN6:45 for T, S, V being non empty TopSpace for P1 being non empty Subset of S for P2 being Subset of S for f being Function of T,(S | P1) for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds ex h being Function of T,V st ( h = g * f & h is continuous ) proof let T, S, V be non empty TopSpace; ::_thesis: for P1 being non empty Subset of S for P2 being Subset of S for f being Function of T,(S | P1) for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds ex h being Function of T,V st ( h = g * f & h is continuous ) let P1 be non empty Subset of S; ::_thesis: for P2 being Subset of S for f being Function of T,(S | P1) for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds ex h being Function of T,V st ( h = g * f & h is continuous ) let P2 be Subset of S; ::_thesis: for f being Function of T,(S | P1) for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds ex h being Function of T,V st ( h = g * f & h is continuous ) let f be Function of T,(S | P1); ::_thesis: for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds ex h being Function of T,V st ( h = g * f & h is continuous ) let g be Function of (S | P2),V; ::_thesis: ( P1 c= P2 & f is continuous & g is continuous implies ex h being Function of T,V st ( h = g * f & h is continuous ) ) assume that A1: P1 c= P2 and A2: f is continuous and A3: g is continuous ; ::_thesis: ex h being Function of T,V st ( h = g * f & h is continuous ) reconsider P3 = P2 as non empty Subset of S by A1, XBOOLE_1:3; A4: [#] (S | P1) = P1 by PRE_TOPC:def_5; A5: [#] (S | P2) = P2 by PRE_TOPC:def_5; then reconsider f1 = f as Function of T,(S | P3) by A1, A4, FUNCT_2:7; for F1 being Subset of (S | P2) st F1 is closed holds f1 " F1 is closed proof let F1 be Subset of (S | P2); ::_thesis: ( F1 is closed implies f1 " F1 is closed ) assume A6: F1 is closed ; ::_thesis: f1 " F1 is closed reconsider P19 = P1 as non empty Subset of (S | P3) by A1, A5; A7: [#] (S | P1) = P1 by PRE_TOPC:def_5; reconsider P4 = F1 /\ P19 as Subset of ((S | P3) | P19) by TOPS_2:29; A8: S | P1 = (S | P3) | P19 by A1, PRE_TOPC:7; A9: P4 is closed by A6, Th2; f1 " P1 = the carrier of T by A7, FUNCT_2:40 .= dom f1 by FUNCT_2:def_1 ; then f1 " F1 = (f1 " F1) /\ (f1 " P1) by RELAT_1:132, XBOOLE_1:28 .= f " P4 by FUNCT_1:68 ; hence f1 " F1 is closed by A2, A8, A9, PRE_TOPC:def_6; ::_thesis: verum end; then f1 is continuous by PRE_TOPC:def_6; hence ex h being Function of T,V st ( h = g * f & h is continuous ) by A3; ::_thesis: verum end; theorem Th46: :: JORDAN6:46 for n being Element of NAT for P1, P2 being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1 = P2 proof let n be Element of NAT ; ::_thesis: for P1, P2 being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1 = P2 let P1, P2 be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds P1 = P2 let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 implies P1 = P2 ) assume that A1: P1 is_an_arc_of p1,p2 and A2: P2 is_an_arc_of p1,p2 and A3: P1 c= P2 ; ::_thesis: P1 = P2 reconsider P19 = P1, P29 = P2 as non empty Subset of (TOP-REAL n) by A1, A2, TOPREAL1:1; now__::_thesis:_not_P2_\_P1_<>_{} assume A4: P2 \ P1 <> {} ; ::_thesis: contradiction set p = the Element of P2 \ P1; A5: the Element of P2 \ P1 in P2 by A4, XBOOLE_0:def_5; A6: not the Element of P2 \ P1 in P1 by A4, XBOOLE_0:def_5; consider f1 being Function of I[01],((TOP-REAL n) | P19) such that A7: f1 is being_homeomorphism and A8: f1 . 0 = p1 and A9: f1 . 1 = p2 by A1, TOPREAL1:def_1; A10: f1 is continuous by A7, TOPS_2:def_5; consider f2 being Function of I[01],((TOP-REAL n) | P29) such that A11: f2 is being_homeomorphism and A12: f2 . 0 = p1 and A13: f2 . 1 = p2 by A2, TOPREAL1:def_1; reconsider f4 = f2 as Function ; A14: f2 is one-to-one by A11, TOPS_2:def_5; A15: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def_5; A16: f2 " is being_homeomorphism by A11, TOPS_2:56; then A17: dom (f2 ") = [#] ((TOP-REAL n) | P2) by TOPS_2:def_5 .= P2 by PRE_TOPC:def_5 ; f2 " is continuous by A11, TOPS_2:def_5; then consider h being Function of I[01],I[01] such that A18: h = (f2 ") * f1 and A19: h is continuous by A3, A10, Th45; reconsider h1 = h as Function of (Closed-Interval-TSpace (0,1)),R^1 by BORSUK_1:40, FUNCT_2:7, TOPMETR:17, TOPMETR:20; for F1 being Subset of R^1 st F1 is closed holds h1 " F1 is closed proof let F1 be Subset of R^1; ::_thesis: ( F1 is closed implies h1 " F1 is closed ) assume A20: F1 is closed ; ::_thesis: h1 " F1 is closed reconsider K = the carrier of I[01] as Subset of R^1 by BORSUK_1:40, TOPMETR:17; A21: I[01] = R^1 | K by BORSUK_1:40, TOPMETR:19, TOPMETR:20; reconsider P3 = F1 /\ K as Subset of (R^1 | K) by TOPS_2:29; A22: P3 is closed by A20, Th2; h1 " K = the carrier of I[01] by FUNCT_2:40 .= dom h1 by FUNCT_2:def_1 ; then h1 " F1 = (h1 " F1) /\ (h1 " K) by RELAT_1:132, XBOOLE_1:28 .= h " P3 by FUNCT_1:68 ; hence h1 " F1 is closed by A19, A21, A22, PRE_TOPC:def_6, TOPMETR:20; ::_thesis: verum end; then reconsider g = h1 as continuous Function of (Closed-Interval-TSpace (0,1)),R^1 by PRE_TOPC:def_6; A23: dom f1 = [#] I[01] by A7, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then A24: 0 in dom f1 by XXREAL_1:1; A25: 1 in dom f1 by A23, XXREAL_1:1; A26: g . 0 = (f2 ") . p1 by A8, A18, A24, FUNCT_1:13; A27: g . 1 = (f2 ") . p2 by A9, A18, A25, FUNCT_1:13; A28: dom f2 = [#] I[01] by A11, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then A29: 0 in dom f2 by XXREAL_1:1; A30: 1 in dom f2 by A28, XXREAL_1:1; A31: f2 is onto by A15, FUNCT_2:def_3; then A32: (f2 ") . p1 = (f4 ") . p1 by A14, TOPS_2:def_4; A33: (f2 ") . p2 = (f4 ") . p2 by A14, A31, TOPS_2:def_4; A34: g . 0 = 0 by A12, A14, A26, A29, A32, FUNCT_1:32; A35: g . 1 = 1 by A13, A14, A27, A30, A33, FUNCT_1:32; the Element of P2 \ P1 in the carrier of ((TOP-REAL n) | P29) by A5, PRE_TOPC:8; then A36: (f2 ") . the Element of P2 \ P1 in the carrier of I[01] by FUNCT_2:5; A37: now__::_thesis:_not_(f2_")_._the_Element_of_P2_\_P1_in_rng_g assume (f2 ") . the Element of P2 \ P1 in rng g ; ::_thesis: contradiction then consider x being set such that A38: x in dom g and A39: (f2 ") . the Element of P2 \ P1 = g . x by FUNCT_1:def_3; A40: (f2 ") . the Element of P2 \ P1 = (f2 ") . (f1 . x) by A18, A38, A39, FUNCT_1:12; A41: x in dom f1 by A18, A38, FUNCT_1:11; A42: f1 . x in dom (f2 ") by A18, A38, FUNCT_1:11; f2 " is one-to-one by A16, TOPS_2:def_5; then the Element of P2 \ P1 = f1 . x by A5, A17, A40, A42, FUNCT_1:def_4; then A43: the Element of P2 \ P1 in rng f1 by A41, FUNCT_1:def_3; rng f1 = [#] ((TOP-REAL n) | P1) by A7, TOPS_2:def_5 .= P1 by PRE_TOPC:def_5 ; hence contradiction by A4, A43, XBOOLE_0:def_5; ::_thesis: verum end; reconsider r = (f2 ") . the Element of P2 \ P1 as Real by A36, BORSUK_1:40; A44: rng f2 = [#] ((TOP-REAL n) | P2) by A11, TOPS_2:def_5 .= P2 by PRE_TOPC:def_5 ; A45: r <= 1 by A36, BORSUK_1:40, XXREAL_1:1; A46: now__::_thesis:_not_r_=_0 assume A47: r = 0 ; ::_thesis: contradiction f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def_4 .= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ; hence contradiction by A1, A6, A12, A47, TOPREAL1:1; ::_thesis: verum end; A48: now__::_thesis:_not_r_=_1 assume A49: r = 1 ; ::_thesis: contradiction f2 . r = f4 . ((f4 ") . the Element of P2 \ P1) by A31, A14, TOPS_2:def_4 .= the Element of P2 \ P1 by A5, A14, A44, FUNCT_1:35 ; hence contradiction by A1, A6, A13, A49, TOPREAL1:1; ::_thesis: verum end; A50: 0 < r by A36, A46, BORSUK_1:40, XXREAL_1:1; r < 1 by A45, A48, XXREAL_0:1; then consider rc being Real such that A51: g . rc = r and A52: 0 < rc and A53: rc < 1 by A34, A35, A50, TOPREAL5:6; the carrier of ((TOP-REAL n) | P1) = [#] ((TOP-REAL n) | P1) .= P1 by PRE_TOPC:def_5 ; then rng f1 c= dom (f2 ") by A3, A17, XBOOLE_1:1; then dom g = dom f1 by A18, RELAT_1:27 .= [#] I[01] by A7, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then rc in dom g by A52, A53, XXREAL_1:1; hence contradiction by A37, A51, FUNCT_1:def_3; ::_thesis: verum end; then P2 c= P1 by XBOOLE_1:37; hence P1 = P2 by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th47: :: JORDAN6:47 for P being Subset of (TOP-REAL 2) for Q being Subset of ((TOP-REAL 2) | P) for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds not Q is connected proof let P be Subset of (TOP-REAL 2); ::_thesis: for Q being Subset of ((TOP-REAL 2) | P) for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds not Q is connected let Q be Subset of ((TOP-REAL 2) | P); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds not Q is connected let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} implies not Q is connected ) assume that A1: P is being_simple_closed_curve and A2: p1 in P and A3: p2 in P and A4: p1 <> p2 and A5: Q = P \ {p1,p2} ; ::_thesis: not Q is connected consider P1, P2 being non empty Subset of (TOP-REAL 2) such that A6: P1 is_an_arc_of p1,p2 and A7: P2 is_an_arc_of p1,p2 and A8: P = P1 \/ P2 and A9: P1 /\ P2 = {p1,p2} by A1, A2, A3, A4, TOPREAL2:5; A10: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; reconsider P = P as Simple_closed_curve by A1; A11: P1 c= P by A8, XBOOLE_1:7; P1 \ {p1,p2} c= P1 by XBOOLE_1:36; then reconsider P19 = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A10, A11, XBOOLE_1:1; A12: P2 c= P by A8, XBOOLE_1:7; P2 \ {p1,p2} c= P2 by XBOOLE_1:36; then reconsider P29 = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A10, A12, XBOOLE_1:1; A13: P19 is open by A7, A8, A9, Th39; A14: P29 is open by A6, A8, A9, Th39; A15: Q c= P19 \/ P29 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in P19 \/ P29 ) assume A16: x in Q ; ::_thesis: x in P19 \/ P29 then A17: x in P by A5, XBOOLE_0:def_5; now__::_thesis:_(_(_x_in_P1_&_not_x_in_{p1,p2}_&_x_in_P19_\/_P29_)_or_(_x_in_P2_&_not_x_in_{p1,p2}_&_x_in_P19_\/_P29_)_) percases ( ( x in P1 & not x in {p1,p2} ) or ( x in P2 & not x in {p1,p2} ) ) by A5, A8, A16, A17, XBOOLE_0:def_3, XBOOLE_0:def_5; case ( x in P1 & not x in {p1,p2} ) ; ::_thesis: x in P19 \/ P29 then x in P19 by XBOOLE_0:def_5; hence x in P19 \/ P29 by XBOOLE_0:def_3; ::_thesis: verum end; case ( x in P2 & not x in {p1,p2} ) ; ::_thesis: x in P19 \/ P29 then x in P29 by XBOOLE_0:def_5; hence x in P19 \/ P29 by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence x in P19 \/ P29 ; ::_thesis: verum end; consider p3 being Point of (TOP-REAL 2) such that A18: p3 in P1 and A19: p3 <> p1 and A20: p3 <> p2 by A6, Th42; not p3 in {p1,p2} by A19, A20, TARSKI:def_2; then A21: P19 <> {} by A18, XBOOLE_0:def_5; P19 c= Q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P19 or x in Q ) assume A22: x in P19 ; ::_thesis: x in Q then A23: x in P1 by XBOOLE_0:def_5; A24: not x in {p1,p2} by A22, XBOOLE_0:def_5; x in P by A8, A23, XBOOLE_0:def_3; hence x in Q by A5, A24, XBOOLE_0:def_5; ::_thesis: verum end; then P19 /\ Q <> {} by A21, XBOOLE_1:28; then A25: P19 meets Q by XBOOLE_0:def_7; consider p39 being Point of (TOP-REAL 2) such that A26: p39 in P2 and A27: p39 <> p1 and A28: p39 <> p2 by A7, Th42; not p39 in {p1,p2} by A27, A28, TARSKI:def_2; then A29: P29 <> {} by A26, XBOOLE_0:def_5; P29 c= Q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P29 or x in Q ) assume A30: x in P29 ; ::_thesis: x in Q then A31: x in P2 by XBOOLE_0:def_5; A32: not x in {p1,p2} by A30, XBOOLE_0:def_5; x in P1 \/ P2 by A31, XBOOLE_0:def_3; hence x in Q by A5, A8, A32, XBOOLE_0:def_5; ::_thesis: verum end; then P29 /\ Q <> {} by A29, XBOOLE_1:28; then A33: P29 meets Q by XBOOLE_0:def_7; now__::_thesis:_not_P19_meets_P29 assume P19 meets P29 ; ::_thesis: contradiction then consider p0 being set such that A34: p0 in P19 and A35: p0 in P29 by XBOOLE_0:3; A36: p0 in P1 by A34, XBOOLE_0:def_5; A37: not p0 in {p1,p2} by A34, XBOOLE_0:def_5; p0 in P2 by A35, XBOOLE_0:def_5; hence contradiction by A9, A36, A37, XBOOLE_0:def_4; ::_thesis: verum end; hence not Q is connected by A13, A14, A15, A25, A33, TOPREAL5:1; ::_thesis: verum end; theorem Th48: :: JORDAN6:48 for P, P1, P2, P19, P29 being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds ( P1 = P29 & P2 = P19 ) proof let P, P1, P2, P19, P29 be Subset of the carrier of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds ( P1 = P29 & P2 = P19 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) implies ( P1 = P29 & P2 = P19 ) ) assume that A1: P is being_simple_closed_curve and A2: P1 is_an_arc_of p1,p2 and A3: P2 is_an_arc_of p1,p2 and A4: P1 \/ P2 = P and A5: P19 is_an_arc_of p1,p2 and A6: P29 is_an_arc_of p1,p2 and A7: P19 \/ P29 = P ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) reconsider P = P as Simple_closed_curve by A1; A8: p1 <> p2 by A6, Th37; A9: p1 in P19 by A5, TOPREAL1:1; A10: p2 in P19 by A5, TOPREAL1:1; A11: p1 in P2 by A3, TOPREAL1:1; A12: p2 in P2 by A3, TOPREAL1:1; A13: p1 in P1 by A2, TOPREAL1:1; A14: p2 in P1 by A2, TOPREAL1:1; A15: P1 c= P by A4, XBOOLE_1:7; A16: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; P1 \ {p1,p2} c= P1 by XBOOLE_1:36; then reconsider Q1 = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A15, A16, XBOOLE_1:1; A17: P2 c= P by A4, XBOOLE_1:7; P2 \ {p1,p2} c= P2 by XBOOLE_1:36; then reconsider Q2 = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A17, XBOOLE_1:1; A18: P19 c= P by A7, XBOOLE_1:7; P19 \ {p1,p2} c= P19 by XBOOLE_1:36; then reconsider Q19 = P19 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A18, XBOOLE_1:1; A19: P29 c= P by A7, XBOOLE_1:7; P29 \ {p1,p2} c= P29 by XBOOLE_1:36; then reconsider Q29 = P29 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A16, A19, XBOOLE_1:1; A20: Q1 \/ Q2 = P \ {p1,p2} by A4, XBOOLE_1:42; A21: Q19 \/ Q29 = P \ {p1,p2} by A7, XBOOLE_1:42; then A22: Q19 \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, XBOOLE_1:7, XBOOLE_1:12; A23: Q29 \/ (Q1 \/ Q2) = Q1 \/ Q2 by A20, A21, XBOOLE_1:7, XBOOLE_1:12; A24: Q1 \/ (Q19 \/ Q29) = Q19 \/ Q29 by A20, A21, XBOOLE_1:7, XBOOLE_1:12; A25: Q2 \/ (Q19 \/ Q29) = Q19 \/ Q29 by A20, A21, XBOOLE_1:7, XBOOLE_1:12; [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5; then reconsider R1 = Q1 as Subset of ((TOP-REAL 2) | P1) by XBOOLE_1:36; R1 is connected by A2, Th40; then A26: Q1 is connected by A4, Th41, XBOOLE_1:7; [#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def_5; then reconsider R2 = Q2 as Subset of ((TOP-REAL 2) | P2) by XBOOLE_1:36; R2 is connected by A3, Th40; then A27: Q2 is connected by A4, Th41, XBOOLE_1:7; [#] ((TOP-REAL 2) | P19) = P19 by PRE_TOPC:def_5; then reconsider R19 = Q19 as Subset of ((TOP-REAL 2) | P19) by XBOOLE_1:36; R19 is connected by A5, Th40; then A28: Q19 is connected by A7, Th41, XBOOLE_1:7; [#] ((TOP-REAL 2) | P29) = P29 by PRE_TOPC:def_5; then reconsider R29 = Q29 as Subset of ((TOP-REAL 2) | P29) by XBOOLE_1:36; R29 is connected by A6, Th40; then A29: Q29 is connected by A7, Th41, XBOOLE_1:7; A30: {p1,p2} c= P1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P1 ) assume x in {p1,p2} ; ::_thesis: x in P1 hence x in P1 by A13, A14, TARSKI:def_2; ::_thesis: verum end; A31: {p1,p2} c= P2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P2 ) assume x in {p1,p2} ; ::_thesis: x in P2 hence x in P2 by A11, A12, TARSKI:def_2; ::_thesis: verum end; A32: {p1,p2} c= P19 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P19 ) assume x in {p1,p2} ; ::_thesis: x in P19 hence x in P19 by A9, A10, TARSKI:def_2; ::_thesis: verum end; A33: {p1,p2} c= P29 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p1,p2} or x in P29 ) assume x in {p1,p2} ; ::_thesis: x in P29 then ( x = p1 or x = p2 ) by TARSKI:def_2; hence x in P29 by A6, TOPREAL1:1; ::_thesis: verum end; A34: Q1 \/ {p1,p2} = P1 by A30, XBOOLE_1:45; A35: Q2 \/ {p1,p2} = P2 by A31, XBOOLE_1:45; A36: Q19 \/ {p1,p2} = P19 by A32, XBOOLE_1:45; A37: Q29 \/ {p1,p2} = P29 by A33, XBOOLE_1:45; now__::_thesis:_(_(_not_P1_=_P29_or_not_P2_=_P19_)_&_not_(_P1_=_P19_&_P2_=_P29_)_implies_(_P1_=_P29_&_P2_=_P19_)_) assume A38: ( not P1 = P29 or not P2 = P19 ) ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) now__::_thesis:_(_(_P1_<>_P29_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_or_(_P2_<>_P19_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_) percases ( P1 <> P29 or P2 <> P19 ) by A38; caseA39: P1 <> P29 ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) A40: now__::_thesis:_(_Q1_\_Q29_=_{}_implies_not_Q29_\_Q1_=_{}_) assume that A41: Q1 \ Q29 = {} and A42: Q29 \ Q1 = {} ; ::_thesis: contradiction A43: Q1 c= Q29 by A41, XBOOLE_1:37; Q29 c= Q1 by A42, XBOOLE_1:37; hence contradiction by A34, A37, A39, A43, XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_(_(_Q1_\_Q29_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_or_(_Q29_\_Q1_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_) percases ( Q1 \ Q29 <> {} or Q29 \ Q1 <> {} ) by A40; caseA44: Q1 \ Q29 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) set y = the Element of Q1 \ Q29; A45: the Element of Q1 \ Q29 in Q1 by A44, XBOOLE_0:def_5; then A46: the Element of Q1 \ Q29 in Q19 \/ Q29 by A20, A21, XBOOLE_0:def_3; not the Element of Q1 \ Q29 in Q29 by A44, XBOOLE_0:def_5; then the Element of Q1 \ Q29 in Q19 by A46, XBOOLE_0:def_3; then Q1 /\ Q19 <> {} by A45, XBOOLE_0:def_4; then A47: Q1 meets Q19 by XBOOLE_0:def_7; now__::_thesis:_not_Q2_meets_Q19 assume Q2 meets Q19 ; ::_thesis: contradiction then (Q1 \/ Q19) \/ Q2 is connected by A26, A27, A28, A47, JORDAN1:4; hence contradiction by A8, A13, A14, A15, A20, A22, Th47, XBOOLE_1:4; ::_thesis: verum end; then A48: Q2 /\ Q19 = {} by XBOOLE_0:def_7; A49: Q2 c= Q29 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q2 or x in Q29 ) assume A50: x in Q2 ; ::_thesis: x in Q29 then x in Q1 \/ Q2 by XBOOLE_0:def_3; then ( x in Q19 or x in Q29 ) by A20, A21, XBOOLE_0:def_3; hence x in Q29 by A48, A50, XBOOLE_0:def_4; ::_thesis: verum end; Q19 c= Q1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q19 or x in Q1 ) assume A51: x in Q19 ; ::_thesis: x in Q1 then x in Q1 \/ Q2 by A20, A21, XBOOLE_0:def_3; then ( x in Q1 or x in Q2 ) by XBOOLE_0:def_3; hence x in Q1 by A48, A51, XBOOLE_0:def_4; ::_thesis: verum end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A49, Th46, XBOOLE_1:9; ::_thesis: verum end; caseA52: Q29 \ Q1 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) set y = the Element of Q29 \ Q1; A53: the Element of Q29 \ Q1 in Q29 by A52, XBOOLE_0:def_5; then A54: the Element of Q29 \ Q1 in Q2 \/ Q1 by A20, A21, XBOOLE_0:def_3; not the Element of Q29 \ Q1 in Q1 by A52, XBOOLE_0:def_5; then the Element of Q29 \ Q1 in Q2 by A54, XBOOLE_0:def_3; then Q29 /\ Q2 <> {} by A53, XBOOLE_0:def_4; then A55: Q29 meets Q2 by XBOOLE_0:def_7; now__::_thesis:_not_Q19_meets_Q2 assume Q19 meets Q2 ; ::_thesis: contradiction then (Q29 \/ Q2) \/ Q19 is connected by A27, A28, A29, A55, JORDAN1:4; hence contradiction by A8, A13, A14, A15, A21, A25, Th47, XBOOLE_1:4; ::_thesis: verum end; then A56: Q19 /\ Q2 = {} by XBOOLE_0:def_7; A57: Q19 c= Q1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q19 or x in Q1 ) assume A58: x in Q19 ; ::_thesis: x in Q1 then x in Q19 \/ Q29 by XBOOLE_0:def_3; then ( x in Q1 or x in Q2 ) by A20, A21, XBOOLE_0:def_3; hence x in Q1 by A56, A58, XBOOLE_0:def_4; ::_thesis: verum end; Q2 c= Q29 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q2 or x in Q29 ) assume A59: x in Q2 ; ::_thesis: x in Q29 then x in Q2 \/ Q1 by XBOOLE_0:def_3; then ( x in Q29 or x in Q19 ) by A20, A21, XBOOLE_0:def_3; hence x in Q29 by A56, A59, XBOOLE_0:def_4; ::_thesis: verum end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A57, Th46, XBOOLE_1:9; ::_thesis: verum end; end; end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum end; caseA60: P2 <> P19 ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) A61: now__::_thesis:_(_Q2_\_Q19_=_{}_implies_not_Q19_\_Q2_=_{}_) assume that A62: Q2 \ Q19 = {} and A63: Q19 \ Q2 = {} ; ::_thesis: contradiction A64: Q2 c= Q19 by A62, XBOOLE_1:37; Q19 c= Q2 by A63, XBOOLE_1:37; hence contradiction by A35, A36, A60, A64, XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_(_(_Q2_\_Q19_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_or_(_Q19_\_Q2_<>_{}_&_(_(_P1_=_P19_&_P2_=_P29_)_or_(_P1_=_P29_&_P2_=_P19_)_)_)_) percases ( Q2 \ Q19 <> {} or Q19 \ Q2 <> {} ) by A61; caseA65: Q2 \ Q19 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) set y = the Element of Q2 \ Q19; A66: the Element of Q2 \ Q19 in Q2 by A65, XBOOLE_0:def_5; then A67: the Element of Q2 \ Q19 in Q29 \/ Q19 by A20, A21, XBOOLE_0:def_3; not the Element of Q2 \ Q19 in Q19 by A65, XBOOLE_0:def_5; then the Element of Q2 \ Q19 in Q29 by A67, XBOOLE_0:def_3; then Q2 /\ Q29 <> {} by A66, XBOOLE_0:def_4; then A68: Q2 meets Q29 by XBOOLE_0:def_7; now__::_thesis:_not_Q1_meets_Q29 assume Q1 meets Q29 ; ::_thesis: contradiction then (Q2 \/ Q29) \/ Q1 is connected by A26, A27, A29, A68, JORDAN1:4; hence contradiction by A8, A13, A14, A15, A20, A23, Th47, XBOOLE_1:4; ::_thesis: verum end; then A69: Q1 /\ Q29 = {} by XBOOLE_0:def_7; A70: Q1 c= Q19 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q1 or x in Q19 ) assume A71: x in Q1 ; ::_thesis: x in Q19 then x in Q2 \/ Q1 by XBOOLE_0:def_3; then ( x in Q29 or x in Q19 ) by A20, A21, XBOOLE_0:def_3; hence x in Q19 by A69, A71, XBOOLE_0:def_4; ::_thesis: verum end; Q29 c= Q2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q29 or x in Q2 ) assume A72: x in Q29 ; ::_thesis: x in Q2 then x in Q2 \/ Q1 by A20, A21, XBOOLE_0:def_3; then ( x in Q2 or x in Q1 ) by XBOOLE_0:def_3; hence x in Q2 by A69, A72, XBOOLE_0:def_4; ::_thesis: verum end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A70, Th46, XBOOLE_1:9; ::_thesis: verum end; caseA73: Q19 \ Q2 <> {} ; ::_thesis: ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) set y = the Element of Q19 \ Q2; A74: the Element of Q19 \ Q2 in Q19 by A73, XBOOLE_0:def_5; then A75: the Element of Q19 \ Q2 in Q1 \/ Q2 by A20, A21, XBOOLE_0:def_3; not the Element of Q19 \ Q2 in Q2 by A73, XBOOLE_0:def_5; then the Element of Q19 \ Q2 in Q1 by A75, XBOOLE_0:def_3; then Q19 /\ Q1 <> {} by A74, XBOOLE_0:def_4; then A76: Q19 meets Q1 by XBOOLE_0:def_7; now__::_thesis:_not_Q29_meets_Q1 assume Q29 meets Q1 ; ::_thesis: contradiction then (Q19 \/ Q1) \/ Q29 is connected by A26, A28, A29, A76, JORDAN1:4; hence contradiction by A8, A13, A14, A15, A21, A24, Th47, XBOOLE_1:4; ::_thesis: verum end; then A77: Q29 /\ Q1 = {} by XBOOLE_0:def_7; A78: Q29 c= Q2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q29 or x in Q2 ) assume A79: x in Q29 ; ::_thesis: x in Q2 then x in Q29 \/ Q19 by XBOOLE_0:def_3; then ( x in Q2 or x in Q1 ) by A20, A21, XBOOLE_0:def_3; hence x in Q2 by A77, A79, XBOOLE_0:def_4; ::_thesis: verum end; Q1 c= Q19 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q1 or x in Q19 ) assume A80: x in Q1 ; ::_thesis: x in Q19 then x in Q19 \/ Q29 by A20, A21, XBOOLE_0:def_3; then ( x in Q19 or x in Q29 ) by XBOOLE_0:def_3; hence x in Q19 by A77, A80, XBOOLE_0:def_4; ::_thesis: verum end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) by A2, A3, A5, A6, A34, A35, A36, A37, A78, Th46, XBOOLE_1:9; ::_thesis: verum end; end; end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum end; end; end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum end; hence ( ( P1 = P19 & P2 = P29 ) or ( P1 = P29 & P2 = P19 ) ) ; ::_thesis: verum end; begin Lm1: for g being Function of I[01],R^1 for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] holds ex r1 being Real st ( 0 < r1 & r1 < 1 & g . r1 = r ) proof let g be Function of I[01],R^1; ::_thesis: for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] holds ex r1 being Real st ( 0 < r1 & r1 < 1 & g . r1 = r ) let s1, s2, r be real number ; ::_thesis: ( g is continuous & g . 0[01] < r & r < g . 1[01] implies ex r1 being Real st ( 0 < r1 & r1 < 1 & g . r1 = r ) ) assume that A1: g is continuous and A2: g . 0[01] < r and A3: r < g . 1[01] ; ::_thesis: ex r1 being Real st ( 0 < r1 & r1 < 1 & g . r1 = r ) ex rc being Real st ( g . rc = r & 0 < rc & rc < 1 ) by A1, A2, A3, BORSUK_1:def_14, BORSUK_1:def_15, TOPMETR:20, TOPREAL5:6; hence ex r1 being Real st ( 0 < r1 & r1 < 1 & g . r1 = r ) ; ::_thesis: verum end; theorem Th49: :: JORDAN6:49 for P1 being Subset of (TOP-REAL 2) for r being real number for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) proof let P1 be Subset of (TOP-REAL 2); ::_thesis: for r being real number for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) let r be real number ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 holds ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 `1 <= r & r <= p2 `1 & P1 is_an_arc_of p1,p2 implies ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) ) assume that A1: p1 `1 <= r and A2: r <= p2 `1 and A3: P1 is_an_arc_of p1,p2 ; ::_thesis: ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) reconsider P19 = P1 as non empty Subset of (TOP-REAL 2) by A3, TOPREAL1:1; consider f being Function of I[01],((TOP-REAL 2) | P19) such that A4: f is being_homeomorphism and A5: f . 0 = p1 and A6: f . 1 = p2 by A3, TOPREAL1:def_1; A7: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5; then reconsider f1 = f as Function of the carrier of I[01], the carrier of (TOP-REAL 2) by FUNCT_2:7; reconsider f2 = f1 as Function of I[01],(TOP-REAL 2) ; reconsider proj11 = proj1 as Function of the carrier of (TOP-REAL 2),REAL ; reconsider proj12 = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17; reconsider g1 = proj11 * f1 as Function of the carrier of I[01],REAL ; reconsider g = g1 as Function of I[01],R^1 by TOPMETR:17; f is continuous by A4, TOPS_2:def_5; then A8: f2 is continuous by Th3; A9: proj12 is continuous by TOPREAL5:10; A10: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1; then A11: 0 in dom f by XXREAL_1:1; A12: 1 in dom f by A10, XXREAL_1:1; A13: g . 0 = proj1 . p1 by A5, A11, FUNCT_1:13 .= p1 `1 by PSCOMP_1:def_5 ; A14: g . 1 = proj1 . p2 by A6, A12, FUNCT_1:13 .= p2 `1 by PSCOMP_1:def_5 ; reconsider P19 = P19 as non empty Subset of (TOP-REAL 2) ; A15: P19 is closed by A3, COMPTS_1:7, JORDAN5A:1; A16: Vertical_Line r is closed by Th6; now__::_thesis:_(_(_g_._0_=_g_._1_&_P1_meets_Vertical_Line_r_)_or_(_g_._0[01]_=_r_&_P1_meets_Vertical_Line_r_)_or_(_g_._1[01]_=_r_&_P1_meets_Vertical_Line_r_)_or_(_g_._0[01]_<_r_&_r_<_g_._1[01]_&_P1_meets_Vertical_Line_r_)_) percases ( g . 0 = g . 1 or g . 0[01] = r or g . 1[01] = r or ( g . 0[01] < r & r < g . 1[01] ) ) by A1, A2, A13, A14, BORSUK_1:def_14, BORSUK_1:def_15, XXREAL_0:1; case g . 0 = g . 1 ; ::_thesis: P1 meets Vertical_Line r then A17: g . 0 = r by A1, A2, A13, A14, XXREAL_0:1; A18: f . 0 in rng f by A11, FUNCT_1:def_3; then f . 0 in P1 by A7; then reconsider p = f . 0 as Point of (TOP-REAL 2) ; p `1 = proj1 . (f . 0) by PSCOMP_1:def_5 .= r by A11, A17, FUNCT_1:13 ; then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ; hence P1 meets Vertical_Line r by A7, A18, XBOOLE_0:3; ::_thesis: verum end; caseA19: g . 0[01] = r ; ::_thesis: P1 meets Vertical_Line r A20: f . 0 in rng f by A11, FUNCT_1:def_3; then f . 0 in P19 by A7; then reconsider p = f . 0 as Point of (TOP-REAL 2) ; p `1 = proj1 . (f . 0) by PSCOMP_1:def_5 .= r by A11, A19, BORSUK_1:def_14, FUNCT_1:13 ; then f . 0 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ; hence P1 meets Vertical_Line r by A7, A20, XBOOLE_0:3; ::_thesis: verum end; caseA21: g . 1[01] = r ; ::_thesis: P1 meets Vertical_Line r A22: f . 1 in rng f by A12, FUNCT_1:def_3; then f . 1 in P1 by A7; then reconsider p = f . 1 as Point of (TOP-REAL 2) ; p `1 = proj1 . (f . 1) by PSCOMP_1:def_5 .= r by A12, A21, BORSUK_1:def_15, FUNCT_1:13 ; then f . 1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ; hence P1 meets Vertical_Line r by A7, A22, XBOOLE_0:3; ::_thesis: verum end; case ( g . 0[01] < r & r < g . 1[01] ) ; ::_thesis: P1 meets Vertical_Line r then consider r1 being Real such that A23: 0 < r1 and A24: r1 < 1 and A25: g . r1 = r by A8, A9, Lm1; dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1; then A26: r1 in dom f by A23, A24, XXREAL_1:1; A27: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5; A28: f . r1 in rng f by A26, FUNCT_1:def_3; then f . r1 in P19 by A27; then reconsider p = f . r1 as Point of (TOP-REAL 2) ; p `1 = proj1 . (f . r1) by PSCOMP_1:def_5 .= r by A25, A26, FUNCT_1:13 ; then f . r1 in { q where q is Point of (TOP-REAL 2) : q `1 = r } ; hence P1 meets Vertical_Line r by A27, A28, XBOOLE_0:3; ::_thesis: verum end; end; end; hence ( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed ) by A15, A16, TOPS_1:8; ::_thesis: verum end; Lm2: now__::_thesis:_for_P_being_Simple_closed_curve for_P1,_P19_being_non_empty_Subset_of_(TOP-REAL_2)_st_ex_P2_being_non_empty_Subset_of_(TOP-REAL_2)_st_ (_P1_is_an_arc_of_W-min_P,_E-max_P_&_P2_is_an_arc_of_E-max_P,_W-min_P_&_P1_/\_P2_=_{(W-min_P),(E-max_P)}_&_P1_\/_P2_=_P_&_(First_Point_(P1,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_>_(Last_Point_(P2,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_)_&_ex_P29_being_non_empty_Subset_of_(TOP-REAL_2)_st_ (_P19_is_an_arc_of_W-min_P,_E-max_P_&_P29_is_an_arc_of_E-max_P,_W-min_P_&_P19_/\_P29_=_{(W-min_P),(E-max_P)}_&_P19_\/_P29_=_P_&_(First_Point_(P19,(W-min_P),(E-max_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_>_(Last_Point_(P29,(E-max_P),(W-min_P),(Vertical_Line_(((W-bound_P)_+_(E-bound_P))_/_2))))_`2_)_holds_ P1_=_P19 let P be Simple_closed_curve; ::_thesis: for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st ( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds P1 = P19 let P1, P19 be non empty Subset of (TOP-REAL 2); ::_thesis: ( ex P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st ( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) implies P1 = P19 ) assume that A1: ex P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) and A2: ex P29 being non empty Subset of (TOP-REAL 2) st ( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ; ::_thesis: P1 = P19 consider P2 being non empty Subset of (TOP-REAL 2) such that A3: P1 is_an_arc_of W-min P, E-max P and A4: P2 is_an_arc_of E-max P, W-min P and P1 /\ P2 = {(W-min P),(E-max P)} and A5: P1 \/ P2 = P and A6: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A1; A7: P2 is_an_arc_of W-min P, E-max P by A4, JORDAN5B:14; consider P29 being non empty Subset of (TOP-REAL 2) such that A8: P19 is_an_arc_of W-min P, E-max P and A9: P29 is_an_arc_of E-max P, W-min P and P19 /\ P29 = {(W-min P),(E-max P)} and A10: P19 \/ P29 = P and A11: (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A2; A12: P29 is_an_arc_of W-min P, E-max P by A9, JORDAN5B:14; now__::_thesis:_(_P1_=_P29_implies_not_P2_=_P19_) assume that A13: P1 = P29 and A14: P2 = P19 ; ::_thesis: contradiction A15: (W-min P) `1 = W-bound P by EUCLID:52; A16: (E-max P) `1 = E-bound P by EUCLID:52; then A17: (W-min P) `1 < (E-max P) `1 by A15, TOPREAL5:17; then A18: (W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2 by A15, A16, XREAL_1:226; A19: ((W-bound P) + (E-bound P)) / 2 <= (E-max P) `1 by A15, A16, A17, XREAL_1:226; then A20: P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A7, A18, Th49; P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A7, A18, A19, Th49; then A21: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (First_Point (P2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A4, A6, A20, JORDAN5C:18; A22: P29 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A12, A18, A19, Th49; P29 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, A18, A19, Th49; hence contradiction by A9, A11, A13, A14, A21, A22, JORDAN5C:18; ::_thesis: verum end; hence P1 = P19 by A3, A5, A7, A8, A10, A12, Th48; ::_thesis: verum end; definition let P be Subset of (TOP-REAL 2); assume A1: P is being_simple_closed_curve ; func Upper_Arc P -> non empty Subset of (TOP-REAL 2) means :Def8: :: JORDAN6:def 8 ( it is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st ( P2 is_an_arc_of E-max P, W-min P & it /\ P2 = {(W-min P),(E-max P)} & it \/ P2 = P & (First_Point (it,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ); existence ex b1 being non empty Subset of (TOP-REAL 2) st ( b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st ( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) proof ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, Th33; hence ex b1 being non empty Subset of (TOP-REAL 2) st ( b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st ( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st ( P2 is_an_arc_of E-max P, W-min P & b1 /\ P2 = {(W-min P),(E-max P)} & b1 \/ P2 = P & (First_Point (b1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & b2 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st ( P2 is_an_arc_of E-max P, W-min P & b2 /\ P2 = {(W-min P),(E-max P)} & b2 \/ P2 = P & (First_Point (b2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds b1 = b2 by A1, Lm2; end; :: deftheorem Def8 defines Upper_Arc JORDAN6:def_8_:_ for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds for b2 being non empty Subset of (TOP-REAL 2) holds ( b2 = Upper_Arc P iff ( b2 is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st ( P2 is_an_arc_of E-max P, W-min P & b2 /\ P2 = {(W-min P),(E-max P)} & b2 \/ P2 = P & (First_Point (b2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) ); definition let P be Subset of (TOP-REAL 2); assume A1: P is being_simple_closed_curve ; then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8; func Lower_Arc P -> non empty Subset of (TOP-REAL 2) means :Def9: :: JORDAN6:def 9 ( it is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ it = {(W-min P),(E-max P)} & (Upper_Arc P) \/ it = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (it,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ); existence ex b1 being non empty Subset of (TOP-REAL 2) st ( b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, Def8; uniqueness for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & b2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b2 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 holds b1 = b2 proof let P1, P19 be non empty Subset of (TOP-REAL 2); ::_thesis: ( P1 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & P19 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P19 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P19 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P19,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 implies P1 = P19 ) assume that A3: P1 is_an_arc_of E-max P, W-min P and (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} and A4: (Upper_Arc P) \/ P1 = P and (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 and A5: P19 is_an_arc_of E-max P, W-min P and (Upper_Arc P) /\ P19 = {(W-min P),(E-max P)} and A6: (Upper_Arc P) \/ P19 = P and (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P19,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ; ::_thesis: P1 = P19 A7: P1 is_an_arc_of W-min P, E-max P by A3, JORDAN5B:14; P19 is_an_arc_of W-min P, E-max P by A5, JORDAN5B:14; then ( P1 = P19 or ( Upper_Arc P = P19 & P1 = Upper_Arc P ) ) by A1, A2, A4, A6, A7, Th48; hence P1 = P19 ; ::_thesis: verum end; end; :: deftheorem Def9 defines Lower_Arc JORDAN6:def_9_:_ for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds for b2 being non empty Subset of (TOP-REAL 2) holds ( b2 = Lower_Arc P iff ( b2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b2 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ); theorem Th50: :: JORDAN6:50 for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) assume A1: P is being_simple_closed_curve ; ::_thesis: ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8; Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9; hence ( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, A2, Def9, JORDAN5B:14; ::_thesis: verum end; theorem Th51: :: JORDAN6:51 for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} ) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} ) ) assume A1: P is being_simple_closed_curve ; ::_thesis: ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} ) then A2: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by Def9; set B = Upper_Arc P; set A = Lower_Arc P; A3: (((Upper_Arc P) \/ (Lower_Arc P)) \ (Upper_Arc P)) \/ ((Upper_Arc P) /\ (Lower_Arc P)) = ((Lower_Arc P) \ (Upper_Arc P)) \/ ((Lower_Arc P) /\ (Upper_Arc P)) by XBOOLE_1:40 .= Lower_Arc P by XBOOLE_1:51 ; (((Upper_Arc P) \/ (Lower_Arc P)) \ (Lower_Arc P)) \/ ((Upper_Arc P) /\ (Lower_Arc P)) = ((Upper_Arc P) \ (Lower_Arc P)) \/ ((Upper_Arc P) /\ (Lower_Arc P)) by XBOOLE_1:40 .= Upper_Arc P by XBOOLE_1:51 ; hence ( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} ) by A1, A2, A3, Def9; ::_thesis: verum end; theorem :: JORDAN6:52 for P being Subset of (TOP-REAL 2) for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds P1 = Lower_Arc P proof let P be Subset of (TOP-REAL 2); ::_thesis: for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds P1 = Lower_Arc P let P1 be Subset of ((TOP-REAL 2) | P); ::_thesis: ( P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P implies P1 = Lower_Arc P ) assume that A1: P is being_simple_closed_curve and A2: (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} and A3: (Upper_Arc P) \/ P1 = P ; ::_thesis: P1 = Lower_Arc P set B = Upper_Arc P; (((Upper_Arc P) \/ P1) \ (Upper_Arc P)) \/ ((Upper_Arc P) /\ P1) = (P1 \ (Upper_Arc P)) \/ (P1 /\ (Upper_Arc P)) by XBOOLE_1:40 .= P1 by XBOOLE_1:51 ; hence P1 = Lower_Arc P by A1, A2, A3, Th51; ::_thesis: verum end; theorem :: JORDAN6:53 for P being Subset of (TOP-REAL 2) for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds P1 = Upper_Arc P proof let P be Subset of (TOP-REAL 2); ::_thesis: for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds P1 = Upper_Arc P let P1 be Subset of ((TOP-REAL 2) | P); ::_thesis: ( P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P implies P1 = Upper_Arc P ) assume that A1: P is being_simple_closed_curve and A2: P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} and A3: P1 \/ (Lower_Arc P) = P ; ::_thesis: P1 = Upper_Arc P set B = Lower_Arc P; ((P1 \/ (Lower_Arc P)) \ (Lower_Arc P)) \/ (P1 /\ (Lower_Arc P)) = (P1 /\ (Lower_Arc P)) \/ (P1 \ (Lower_Arc P)) by XBOOLE_1:40 .= P1 by XBOOLE_1:51 ; hence P1 = Upper_Arc P by A1, A2, A3, Th51; ::_thesis: verum end; begin theorem Th54: :: JORDAN6:54 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds q = p1 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds q = p1 let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 implies q = p1 ) assume that A1: P is_an_arc_of p1,p2 and A2: LE q,p1,P,p1,p2 ; ::_thesis: q = p1 q in P by A2, JORDAN5C:def_3; then LE p1,q,P,p1,p2 by A1, JORDAN5C:10; hence q = p1 by A1, A2, JORDAN5C:12; ::_thesis: verum end; theorem Th55: :: JORDAN6:55 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds q = p2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds q = p2 let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 implies q = p2 ) assume that A1: P is_an_arc_of p1,p2 and A2: LE p2,q,P,p1,p2 ; ::_thesis: q = p2 q in P by A2, JORDAN5C:def_3; then LE q,p2,P,p1,p2 by A1, JORDAN5C:10; hence q = p2 by A1, A2, JORDAN5C:12; ::_thesis: verum end; definition let P be Subset of (TOP-REAL 2); let q1, q2 be Point of (TOP-REAL 2); pred LE q1,q2,P means :Def10: :: JORDAN6:def 10 ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ); end; :: deftheorem Def10 defines LE JORDAN6:def_10_:_ for P being Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) holds ( LE q1,q2,P iff ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ); theorem :: JORDAN6:56 for P being Subset of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds LE q,q,P proof let P be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds LE q,q,P let q be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & q in P implies LE q,q,P ) assume that A1: P is being_simple_closed_curve and A2: q in P ; ::_thesis: LE q,q,P A3: (Upper_Arc P) \/ (Lower_Arc P) = P by A1, Def9; A4: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50; now__::_thesis:_(_(_q_in_Upper_Arc_P_&_LE_q,q,P_)_or_(_q_in_Lower_Arc_P_&_not_q_in_Upper_Arc_P_&_LE_q,q,P_)_) percases ( q in Upper_Arc P or ( q in Lower_Arc P & not q in Upper_Arc P ) ) by A2, A3, XBOOLE_0:def_3; caseA5: q in Upper_Arc P ; ::_thesis: LE q,q,P then LE q,q, Upper_Arc P, W-min P, E-max P by JORDAN5C:9; hence LE q,q,P by A5, Def10; ::_thesis: verum end; caseA6: ( q in Lower_Arc P & not q in Upper_Arc P ) ; ::_thesis: LE q,q,P then A7: LE q,q, Lower_Arc P, E-max P, W-min P by JORDAN5C:9; q <> W-min P by A4, A6, TOPREAL1:1; hence LE q,q,P by A6, A7, Def10; ::_thesis: verum end; end; end; hence LE q,q,P ; ::_thesis: verum end; theorem :: JORDAN6:57 for P being Subset of (TOP-REAL 2) for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds q1 = q2 proof let P be Subset of (TOP-REAL 2); ::_thesis: for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds q1 = q2 let q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P implies q1 = q2 ) assume that A1: P is being_simple_closed_curve and A2: LE q1,q2,P and A3: LE q2,q1,P ; ::_thesis: q1 = q2 A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9; A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9; A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50; now__::_thesis:_(_(_q1_in_Upper_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_q1_=_q2_)_or_(_q1_in_Upper_Arc_P_&_q2_in_Upper_Arc_P_&_LE_q1,q2,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q1_in_Lower_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_LE_q1,q2,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_) percases ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A2, Def10; caseA7: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; ::_thesis: q1 = q2 now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_q1_=_q2_)_or_(_q2_in_Upper_Arc_P_&_q1_in_Upper_Arc_P_&_LE_q2,q1,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q2_in_Lower_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_LE_q2,q1,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_) percases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10; caseA8: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; ::_thesis: q1 = q2 then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4; then A9: q1 = E-max P by A5, A8, TARSKI:def_2; q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, A8, XBOOLE_0:def_4; hence q1 = q2 by A5, A7, A9, TARSKI:def_2; ::_thesis: verum end; caseA10: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2 then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4; then q2 = E-max P by A5, A7, TARSKI:def_2; hence q1 = q2 by A6, A10, Th55; ::_thesis: verum end; caseA11: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2 then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4; then q1 = E-max P by A5, A11, TARSKI:def_2; hence q1 = q2 by A4, A11, Th54; ::_thesis: verum end; end; end; hence q1 = q2 ; ::_thesis: verum end; caseA12: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2 now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_q1_=_q2_)_or_(_q2_in_Upper_Arc_P_&_q1_in_Upper_Arc_P_&_LE_q2,q1,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q2_in_Lower_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_LE_q2,q1,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_) percases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10; caseA13: ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; ::_thesis: q1 = q2 then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def_4; then q1 = E-max P by A5, A13, TARSKI:def_2; hence q1 = q2 by A6, A12, Th55; ::_thesis: verum end; case ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2 hence q1 = q2 by A6, A12, JORDAN5C:12; ::_thesis: verum end; caseA14: ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2 then q1 in (Upper_Arc P) /\ (Lower_Arc P) by A12, XBOOLE_0:def_4; then q1 = E-max P by A5, A14, TARSKI:def_2; hence q1 = q2 by A4, A14, Th54; ::_thesis: verum end; end; end; hence q1 = q2 ; ::_thesis: verum end; caseA15: ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2 now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_q1_=_q2_)_or_(_q2_in_Upper_Arc_P_&_q1_in_Upper_Arc_P_&_LE_q2,q1,_Upper_Arc_P,_W-min_P,_E-max_P_&_q1_=_q2_)_or_(_q2_in_Lower_Arc_P_&_q1_in_Lower_Arc_P_&_not_q1_=_W-min_P_&_LE_q2,q1,_Lower_Arc_P,_E-max_P,_W-min_P_&_q1_=_q2_)_) percases ( ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) or ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10; case ( q2 in Upper_Arc P & q1 in Lower_Arc P & not q1 = W-min P ) ; ::_thesis: q1 = q2 then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A15, XBOOLE_0:def_4; then q2 = E-max P by A5, A15, TARSKI:def_2; hence q1 = q2 by A4, A15, Th54; ::_thesis: verum end; caseA16: ( q2 in Upper_Arc P & q1 in Upper_Arc P & LE q2,q1, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: q1 = q2 then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A15, XBOOLE_0:def_4; then q2 = E-max P by A5, A15, TARSKI:def_2; hence q1 = q2 by A6, A16, Th55; ::_thesis: verum end; case ( q2 in Lower_Arc P & q1 in Lower_Arc P & not q1 = W-min P & LE q2,q1, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: q1 = q2 hence q1 = q2 by A4, A15, JORDAN5C:12; ::_thesis: verum end; end; end; hence q1 = q2 ; ::_thesis: verum end; end; end; hence q1 = q2 ; ::_thesis: verum end; theorem :: JORDAN6:58 for P being Subset of (TOP-REAL 2) for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds LE q1,q3,P proof let P be Subset of (TOP-REAL 2); ::_thesis: for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds LE q1,q3,P let q1, q2, q3 be Point of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P implies LE q1,q3,P ) assume that A1: P is being_simple_closed_curve and A2: LE q1,q2,P and A3: LE q2,q3,P ; ::_thesis: LE q1,q3,P A4: Lower_Arc P is_an_arc_of E-max P, W-min P by A1, Def9; A5: (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} by A1, Def9; A6: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th50; now__::_thesis:_(_(_q1_in_Upper_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_LE_q1,q3,P_)_or_(_q1_in_Upper_Arc_P_&_q2_in_Upper_Arc_P_&_LE_q1,q2,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q1_in_Lower_Arc_P_&_q2_in_Lower_Arc_P_&_not_q2_=_W-min_P_&_LE_q1,q2,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_) percases ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) by A2, Def10; caseA7: ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) ; ::_thesis: LE q1,q3,P now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q1,q3,P_)_or_(_q2_in_Upper_Arc_P_&_q3_in_Upper_Arc_P_&_LE_q2,q3,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q2_in_Lower_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q2,q3,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_) percases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10; case ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; ::_thesis: LE q1,q3,P hence LE q1,q3,P by A7, Def10; ::_thesis: verum end; caseA8: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A7, XBOOLE_0:def_4; then q2 = E-max P by A5, A7, TARSKI:def_2; hence LE q1,q3,P by A2, A6, A8, Th55; ::_thesis: verum end; case ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P hence LE q1,q3,P by A7, Def10; ::_thesis: verum end; end; end; hence LE q1,q3,P ; ::_thesis: verum end; caseA9: ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q1,q3,P_)_or_(_q2_in_Upper_Arc_P_&_q3_in_Upper_Arc_P_&_LE_q2,q3,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q2_in_Lower_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q2,q3,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_) percases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10; case ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; ::_thesis: LE q1,q3,P hence LE q1,q3,P by A9, Def10; ::_thesis: verum end; caseA10: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P then LE q1,q3, Upper_Arc P, W-min P, E-max P by A9, JORDAN5C:13; hence LE q1,q3,P by A9, A10, Def10; ::_thesis: verum end; case ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P hence LE q1,q3,P by A9, Def10; ::_thesis: verum end; end; end; hence LE q1,q3,P ; ::_thesis: verum end; caseA11: ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P now__::_thesis:_(_(_q2_in_Upper_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q1,q3,P_)_or_(_q2_in_Upper_Arc_P_&_q3_in_Upper_Arc_P_&_LE_q2,q3,_Upper_Arc_P,_W-min_P,_E-max_P_&_LE_q1,q3,P_)_or_(_q2_in_Lower_Arc_P_&_q3_in_Lower_Arc_P_&_not_q3_=_W-min_P_&_LE_q2,q3,_Lower_Arc_P,_E-max_P,_W-min_P_&_LE_q1,q3,P_)_) percases ( ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) or ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) or ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ) by A3, Def10; caseA12: ( q2 in Upper_Arc P & q3 in Lower_Arc P & not q3 = W-min P ) ; ::_thesis: LE q1,q3,P then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A11, XBOOLE_0:def_4; then q2 = E-max P by A5, A11, TARSKI:def_2; then LE q2,q3, Lower_Arc P, E-max P, W-min P by A4, A12, JORDAN5C:10; then LE q1,q3, Lower_Arc P, E-max P, W-min P by A11, JORDAN5C:13; hence LE q1,q3,P by A11, A12, Def10; ::_thesis: verum end; caseA13: ( q2 in Upper_Arc P & q3 in Upper_Arc P & LE q2,q3, Upper_Arc P, W-min P, E-max P ) ; ::_thesis: LE q1,q3,P then q2 in (Upper_Arc P) /\ (Lower_Arc P) by A11, XBOOLE_0:def_4; then q2 = E-max P by A5, A11, TARSKI:def_2; hence LE q1,q3,P by A2, A6, A13, Th55; ::_thesis: verum end; caseA14: ( q2 in Lower_Arc P & q3 in Lower_Arc P & not q3 = W-min P & LE q2,q3, Lower_Arc P, E-max P, W-min P ) ; ::_thesis: LE q1,q3,P then LE q1,q3, Lower_Arc P, E-max P, W-min P by A11, JORDAN5C:13; hence LE q1,q3,P by A11, A14, Def10; ::_thesis: verum end; end; end; hence LE q1,q3,P ; ::_thesis: verum end; end; end; hence LE q1,q3,P ; ::_thesis: verum end; theorem :: JORDAN6:59 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p2 holds not p2 in L_Segment (P,p1,p2,q) proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p2 holds not p2 in L_Segment (P,p1,p2,q) let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q <> p2 implies not p2 in L_Segment (P,p1,p2,q) ) assume that A1: P is_an_arc_of p1,p2 and A2: q <> p2 ; ::_thesis: not p2 in L_Segment (P,p1,p2,q) assume p2 in L_Segment (P,p1,p2,q) ; ::_thesis: contradiction then ex w being Point of (TOP-REAL 2) st ( p2 = w & LE w,q,P,p1,p2 ) ; hence contradiction by A1, A2, Th55; ::_thesis: verum end; theorem :: JORDAN6:60 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p1 holds not p1 in R_Segment (P,p1,p2,q) proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p1 holds not p1 in R_Segment (P,p1,p2,q) let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q <> p1 implies not p1 in R_Segment (P,p1,p2,q) ) assume that A1: P is_an_arc_of p1,p2 and A2: q <> p1 ; ::_thesis: not p1 in R_Segment (P,p1,p2,q) assume p1 in R_Segment (P,p1,p2,q) ; ::_thesis: contradiction then ex w being Point of (TOP-REAL 2) st ( p1 = w & LE q,w,P,p1,p2 ) ; hence contradiction by A1, A2, Th54; ::_thesis: verum end; registration let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2); cluster Lower_Arc S -> non empty compact ; coherence ( not Lower_Arc S is empty & Lower_Arc S is compact ) proof Lower_Arc S is_an_arc_of E-max S, W-min S by Def9; hence ( not Lower_Arc S is empty & Lower_Arc S is compact ) by JORDAN5A:1; ::_thesis: verum end; cluster Upper_Arc S -> non empty compact ; coherence ( not Upper_Arc S is empty & Upper_Arc S is compact ) proof Upper_Arc S is_an_arc_of W-min S, E-max S by Def8; hence ( not Upper_Arc S is empty & Upper_Arc S is compact ) by JORDAN5A:1; ::_thesis: verum end; end; theorem Th61: :: JORDAN6:61 for S being non empty being_simple_closed_curve Subset of (TOP-REAL 2) holds ( Lower_Arc S c= S & Upper_Arc S c= S ) proof let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2); ::_thesis: ( Lower_Arc S c= S & Upper_Arc S c= S ) S = (Lower_Arc S) \/ (Upper_Arc S) by Th50; hence ( Lower_Arc S c= S & Upper_Arc S c= S ) by XBOOLE_1:7; ::_thesis: verum end; definition let C be Simple_closed_curve; func Lower_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN6:def 11 First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); coherence First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ; func Upper_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN6:def 12 First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); coherence First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ; end; :: deftheorem defines Lower_Middle_Point JORDAN6:def_11_:_ for C being Simple_closed_curve holds Lower_Middle_Point C = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); :: deftheorem defines Upper_Middle_Point JORDAN6:def_12_:_ for C being Simple_closed_curve holds Upper_Middle_Point C = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); theorem Th62: :: JORDAN6:62 for C being Simple_closed_curve holds Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) proof let C be Simple_closed_curve; ::_thesis: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) A1: W-bound C <= E-bound C by SPRECT_1:21; (W-min C) `1 = W-bound C by EUCLID:52; then A2: (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 by A1, Th1; (E-max C) `1 = E-bound C by EUCLID:52; then A3: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, Th1; Lower_Arc C is_an_arc_of W-min C, E-max C by Th50; hence Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; ::_thesis: verum end; theorem Th63: :: JORDAN6:63 for C being Simple_closed_curve holds Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) proof let C be Simple_closed_curve; ::_thesis: Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) A1: W-bound C <= E-bound C by SPRECT_1:21; (W-min C) `1 = W-bound C by EUCLID:52; then A2: (W-min C) `1 <= ((W-bound C) + (E-bound C)) / 2 by A1, Th1; (E-max C) `1 = E-bound C by EUCLID:52; then A3: ((W-bound C) + (E-bound C)) / 2 <= (E-max C) `1 by A1, Th1; Upper_Arc C is_an_arc_of W-min C, E-max C by Th50; hence Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by A2, A3, Th49; ::_thesis: verum end; theorem :: JORDAN6:64 for C being Simple_closed_curve holds (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 proof let C be Simple_closed_curve; ::_thesis: (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2); set p = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); A1: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th62; Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6; then A2: (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8; Lower_Arc C is_an_arc_of W-min C, E-max C by Th50; then First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A1, A2, JORDAN5C:def_1; then First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by XBOOLE_0:def_4; hence (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by Th31; ::_thesis: verum end; theorem :: JORDAN6:65 for C being Simple_closed_curve holds (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 proof let C be Simple_closed_curve; ::_thesis: (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2); set p = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); A1: Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th63; Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6; then A2: (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8; Upper_Arc C is_an_arc_of W-min C, E-max C by Th50; then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) by A1, A2, JORDAN5C:def_1; then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in Vertical_Line (((W-bound C) + (E-bound C)) / 2) by XBOOLE_0:def_4; hence (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2 by Th31; ::_thesis: verum end; theorem :: JORDAN6:66 for C being Simple_closed_curve holds Lower_Middle_Point C in Lower_Arc C proof let C be Simple_closed_curve; ::_thesis: Lower_Middle_Point C in Lower_Arc C set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2); set p = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); A1: Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th62; Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6; then A2: (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8; Lower_Arc C is_an_arc_of W-min C, E-max C by Th50; then First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) /\ (Lower_Arc C) by A1, A2, JORDAN5C:def_1; hence Lower_Middle_Point C in Lower_Arc C by XBOOLE_0:def_4; ::_thesis: verum end; theorem Th67: :: JORDAN6:67 for C being Simple_closed_curve holds Upper_Middle_Point C in Upper_Arc C proof let C be Simple_closed_curve; ::_thesis: Upper_Middle_Point C in Upper_Arc C set L = Vertical_Line (((W-bound C) + (E-bound C)) / 2); set p = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))); A1: Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2) by Th63; Vertical_Line (((W-bound C) + (E-bound C)) / 2) is closed by Th6; then A2: (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is closed by TOPS_1:8; A3: Upper_Arc C is_an_arc_of E-max C, W-min C by Th50; then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) = Last_Point ((Upper_Arc C),(E-max C),(W-min C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) by A1, A2, JORDAN5C:18; then First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) in (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) /\ (Upper_Arc C) by A1, A2, A3, JORDAN5C:def_2; hence Upper_Middle_Point C in Upper_Arc C by XBOOLE_0:def_4; ::_thesis: verum end; theorem :: JORDAN6:68 for C being Simple_closed_curve holds Upper_Middle_Point C in C proof let C be Simple_closed_curve; ::_thesis: Upper_Middle_Point C in C A1: Upper_Middle_Point C in Upper_Arc C by Th67; Upper_Arc C c= C by Th61; hence Upper_Middle_Point C in C by A1; ::_thesis: verum end; theorem :: JORDAN6:69 for C being Simple_closed_curve for r being real number st W-bound C <= r & r <= E-bound C holds LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C proof let C be Simple_closed_curve; ::_thesis: for r being real number st W-bound C <= r & r <= E-bound C holds LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C let r be real number ; ::_thesis: ( W-bound C <= r & r <= E-bound C implies LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C ) A1: (W-min C) `1 = W-bound C by EUCLID:52; A2: (E-max C) `1 = E-bound C by EUCLID:52; assume that A3: W-bound C <= r and A4: r <= E-bound C ; ::_thesis: LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C Upper_Arc C is_an_arc_of W-min C, E-max C by Def8; then Upper_Arc C meets Vertical_Line r by A1, A2, A3, A4, Th49; then consider x being set such that A5: x in (Upper_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4; A6: x in Upper_Arc C by A5, XBOOLE_0:def_4; A7: x in Vertical_Line r by A5, XBOOLE_0:def_4; reconsider fs = x as Point of (TOP-REAL 2) by A5; A8: Upper_Arc C c= C by Th61; then A9: S-bound C <= fs `2 by A6, PSCOMP_1:24; A10: fs `2 <= N-bound C by A6, A8, PSCOMP_1:24; A11: |[r,(S-bound C)]| `1 = r by EUCLID:52 .= fs `1 by A7, Th31 ; A12: |[r,(N-bound C)]| `1 = r by EUCLID:52 .= fs `1 by A7, Th31 ; A13: |[r,(S-bound C)]| `2 = S-bound C by EUCLID:52; |[r,(N-bound C)]| `2 = N-bound C by EUCLID:52; then x in LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) by A9, A10, A11, A12, A13, GOBOARD7:7; hence LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C by A6, XBOOLE_0:3; ::_thesis: verum end; theorem :: JORDAN6:70 for C being Simple_closed_curve for r being real number st W-bound C <= r & r <= E-bound C holds LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C proof let C be Simple_closed_curve; ::_thesis: for r being real number st W-bound C <= r & r <= E-bound C holds LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C let r be real number ; ::_thesis: ( W-bound C <= r & r <= E-bound C implies LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C ) A1: (W-min C) `1 = W-bound C by EUCLID:52; A2: (E-max C) `1 = E-bound C by EUCLID:52; assume that A3: W-bound C <= r and A4: r <= E-bound C ; ::_thesis: LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C Lower_Arc C is_an_arc_of E-max C, W-min C by Def9; then Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN5B:14; then Lower_Arc C meets Vertical_Line r by A1, A2, A3, A4, Th49; then consider x being set such that A5: x in (Lower_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4; A6: x in Lower_Arc C by A5, XBOOLE_0:def_4; A7: x in Vertical_Line r by A5, XBOOLE_0:def_4; reconsider fs = x as Point of (TOP-REAL 2) by A5; A8: Lower_Arc C c= C by Th61; then A9: S-bound C <= fs `2 by A6, PSCOMP_1:24; A10: fs `2 <= N-bound C by A6, A8, PSCOMP_1:24; A11: |[r,(S-bound C)]| `1 = r by EUCLID:52 .= fs `1 by A7, Th31 ; A12: |[r,(N-bound C)]| `1 = r by EUCLID:52 .= fs `1 by A7, Th31 ; A13: |[r,(S-bound C)]| `2 = S-bound C by EUCLID:52; |[r,(N-bound C)]| `2 = N-bound C by EUCLID:52; then x in LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) by A9, A10, A11, A12, A13, GOBOARD7:7; hence LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C by A6, XBOOLE_0:3; ::_thesis: verum end;