:: JORDAN18 semantic presentation begin Lm1: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; Lm2: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; theorem :: JORDAN18:1 for a, b being real number holds (a - b) ^2 = (b - a) ^2 ; theorem :: JORDAN18:2 for S, T being non empty TopStruct for f being Function of S,T for A being Subset of T st f is being_homeomorphism & A is compact holds f " A is compact proof let S, T be non empty TopStruct ; ::_thesis: for f being Function of S,T for A being Subset of T st f is being_homeomorphism & A is compact holds f " A is compact let f be Function of S,T; ::_thesis: for A being Subset of T st f is being_homeomorphism & A is compact holds f " A is compact let A be Subset of T; ::_thesis: ( f is being_homeomorphism & A is compact implies f " A is compact ) assume that A1: f is being_homeomorphism and A2: A is compact ; ::_thesis: f " A is compact A3: ( rng f = [#] T & f is one-to-one ) by A1, TOPS_2:def_5; f " is being_homeomorphism by A1, TOPS_2:56; then A4: rng (f ") = [#] S by TOPS_2:def_5; f " is continuous by A1, TOPS_2:def_5; then (f ") .: A is compact by A2, A4, COMPTS_1:15; hence f " A is compact by A3, TOPS_2:55; ::_thesis: verum end; theorem Th3: :: JORDAN18:3 for a being Point of (TOP-REAL 2) holds proj2 .: (north_halfline a) is bounded_below proof let a be Point of (TOP-REAL 2); ::_thesis: proj2 .: (north_halfline a) is bounded_below take a `2 ; :: according to XXREAL_2:def_9 ::_thesis: a `2 is LowerBound of proj2 .: (north_halfline a) let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in proj2 .: (north_halfline a) or a `2 <= r ) assume r in proj2 .: (north_halfline a) ; ::_thesis: a `2 <= r then consider x being set such that A1: x in the carrier of (TOP-REAL 2) and A2: x in north_halfline a and A3: r = proj2 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A1; r = x `2 by A3, PSCOMP_1:def_6; hence a `2 <= r by A2, TOPREAL1:def_10; ::_thesis: verum end; theorem Th4: :: JORDAN18:4 for a being Point of (TOP-REAL 2) holds proj2 .: (south_halfline a) is bounded_above proof let a be Point of (TOP-REAL 2); ::_thesis: proj2 .: (south_halfline a) is bounded_above take a `2 ; :: according to XXREAL_2:def_10 ::_thesis: a `2 is UpperBound of proj2 .: (south_halfline a) let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in proj2 .: (south_halfline a) or r <= a `2 ) assume r in proj2 .: (south_halfline a) ; ::_thesis: r <= a `2 then consider x being set such that A1: x in the carrier of (TOP-REAL 2) and A2: x in south_halfline a and A3: r = proj2 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A1; r = x `2 by A3, PSCOMP_1:def_6; hence r <= a `2 by A2, TOPREAL1:def_12; ::_thesis: verum end; theorem Th5: :: JORDAN18:5 for a being Point of (TOP-REAL 2) holds proj1 .: (west_halfline a) is bounded_above proof let a be Point of (TOP-REAL 2); ::_thesis: proj1 .: (west_halfline a) is bounded_above take a `1 ; :: according to XXREAL_2:def_10 ::_thesis: a `1 is UpperBound of proj1 .: (west_halfline a) let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in proj1 .: (west_halfline a) or r <= a `1 ) assume r in proj1 .: (west_halfline a) ; ::_thesis: r <= a `1 then consider x being set such that A1: x in the carrier of (TOP-REAL 2) and A2: x in west_halfline a and A3: r = proj1 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A1; r = x `1 by A3, PSCOMP_1:def_5; hence r <= a `1 by A2, TOPREAL1:def_13; ::_thesis: verum end; theorem Th6: :: JORDAN18:6 for a being Point of (TOP-REAL 2) holds proj1 .: (east_halfline a) is bounded_below proof let a be Point of (TOP-REAL 2); ::_thesis: proj1 .: (east_halfline a) is bounded_below take a `1 ; :: according to XXREAL_2:def_9 ::_thesis: a `1 is LowerBound of proj1 .: (east_halfline a) let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in proj1 .: (east_halfline a) or a `1 <= r ) assume r in proj1 .: (east_halfline a) ; ::_thesis: a `1 <= r then consider x being set such that A1: x in the carrier of (TOP-REAL 2) and A2: x in east_halfline a and A3: r = proj1 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A1; r = x `1 by A3, PSCOMP_1:def_5; hence a `1 <= r by A2, TOPREAL1:def_11; ::_thesis: verum end; registration let a be Point of (TOP-REAL 2); clusterproj2 .: (north_halfline a) -> non empty ; coherence not proj2 .: (north_halfline a) is empty by Lm2, RELAT_1:119; clusterproj2 .: (south_halfline a) -> non empty ; coherence not proj2 .: (south_halfline a) is empty by Lm2, RELAT_1:119; clusterproj1 .: (west_halfline a) -> non empty ; coherence not proj1 .: (west_halfline a) is empty by Lm1, RELAT_1:119; clusterproj1 .: (east_halfline a) -> non empty ; coherence not proj1 .: (east_halfline a) is empty by Lm1, RELAT_1:119; end; theorem Th7: :: JORDAN18:7 for a being Point of (TOP-REAL 2) holds lower_bound (proj2 .: (north_halfline a)) = a `2 proof let a be Point of (TOP-REAL 2); ::_thesis: lower_bound (proj2 .: (north_halfline a)) = a `2 set X = proj2 .: (north_halfline a); A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj2_.:_(north_halfline_a)_holds_ a_`2_<=_r let r be real number ; ::_thesis: ( r in proj2 .: (north_halfline a) implies a `2 <= r ) assume r in proj2 .: (north_halfline a) ; ::_thesis: a `2 <= r then consider x being set such that A2: x in the carrier of (TOP-REAL 2) and A3: x in north_halfline a and A4: r = proj2 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A2; r = x `2 by A4, PSCOMP_1:def_6; hence a `2 <= r by A3, TOPREAL1:def_10; ::_thesis: verum end; A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r_being_real_number_st_ (_r_in_proj2_.:_(north_halfline_a)_&_r_<_(a_`2)_+_s_) reconsider r = a `2 as real number ; let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in proj2 .: (north_halfline a) & r < (a `2) + s ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in proj2 .: (north_halfline a) & r < (a `2) + s ) then A6: r + 0 < (a `2) + s by XREAL_1:8; take r = r; ::_thesis: ( r in proj2 .: (north_halfline a) & r < (a `2) + s ) ( a in north_halfline a & r = proj2 . a ) by PSCOMP_1:def_6, TOPREAL1:38; hence r in proj2 .: (north_halfline a) by FUNCT_2:35; ::_thesis: r < (a `2) + s thus r < (a `2) + s by A6; ::_thesis: verum end; proj2 .: (north_halfline a) is bounded_below by Th3; hence lower_bound (proj2 .: (north_halfline a)) = a `2 by A1, A5, SEQ_4:def_2; ::_thesis: verum end; theorem Th8: :: JORDAN18:8 for a being Point of (TOP-REAL 2) holds upper_bound (proj2 .: (south_halfline a)) = a `2 proof let a be Point of (TOP-REAL 2); ::_thesis: upper_bound (proj2 .: (south_halfline a)) = a `2 set X = proj2 .: (south_halfline a); A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj2_.:_(south_halfline_a)_holds_ r_<=_a_`2 let r be real number ; ::_thesis: ( r in proj2 .: (south_halfline a) implies r <= a `2 ) assume r in proj2 .: (south_halfline a) ; ::_thesis: r <= a `2 then consider x being set such that A2: x in the carrier of (TOP-REAL 2) and A3: x in south_halfline a and A4: r = proj2 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A2; r = x `2 by A4, PSCOMP_1:def_6; hence r <= a `2 by A3, TOPREAL1:def_12; ::_thesis: verum end; A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r_being_real_number_st_ (_r_in_proj2_.:_(south_halfline_a)_&_(a_`2)_-_s_<_r_) reconsider r = a `2 as real number ; let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in proj2 .: (south_halfline a) & (a `2) - s < r ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in proj2 .: (south_halfline a) & (a `2) - s < r ) then A6: (a `2) - s < r - 0 by XREAL_1:15; take r = r; ::_thesis: ( r in proj2 .: (south_halfline a) & (a `2) - s < r ) ( a in south_halfline a & r = proj2 . a ) by PSCOMP_1:def_6, TOPREAL1:38; hence r in proj2 .: (south_halfline a) by FUNCT_2:35; ::_thesis: (a `2) - s < r thus (a `2) - s < r by A6; ::_thesis: verum end; proj2 .: (south_halfline a) is bounded_above by Th4; hence upper_bound (proj2 .: (south_halfline a)) = a `2 by A1, A5, SEQ_4:def_1; ::_thesis: verum end; theorem :: JORDAN18:9 for a being Point of (TOP-REAL 2) holds upper_bound (proj1 .: (west_halfline a)) = a `1 proof let a be Point of (TOP-REAL 2); ::_thesis: upper_bound (proj1 .: (west_halfline a)) = a `1 set X = proj1 .: (west_halfline a); A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj1_.:_(west_halfline_a)_holds_ r_<=_a_`1 let r be real number ; ::_thesis: ( r in proj1 .: (west_halfline a) implies r <= a `1 ) assume r in proj1 .: (west_halfline a) ; ::_thesis: r <= a `1 then consider x being set such that A2: x in the carrier of (TOP-REAL 2) and A3: x in west_halfline a and A4: r = proj1 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A2; r = x `1 by A4, PSCOMP_1:def_5; hence r <= a `1 by A3, TOPREAL1:def_13; ::_thesis: verum end; A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r_being_real_number_st_ (_r_in_proj1_.:_(west_halfline_a)_&_(a_`1)_-_s_<_r_) reconsider r = a `1 as real number ; let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in proj1 .: (west_halfline a) & (a `1) - s < r ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in proj1 .: (west_halfline a) & (a `1) - s < r ) then A6: (a `1) - s < r - 0 by XREAL_1:15; take r = r; ::_thesis: ( r in proj1 .: (west_halfline a) & (a `1) - s < r ) ( a in west_halfline a & r = proj1 . a ) by PSCOMP_1:def_5, TOPREAL1:38; hence r in proj1 .: (west_halfline a) by FUNCT_2:35; ::_thesis: (a `1) - s < r thus (a `1) - s < r by A6; ::_thesis: verum end; proj1 .: (west_halfline a) is bounded_above by Th5; hence upper_bound (proj1 .: (west_halfline a)) = a `1 by A1, A5, SEQ_4:def_1; ::_thesis: verum end; theorem :: JORDAN18:10 for a being Point of (TOP-REAL 2) holds lower_bound (proj1 .: (east_halfline a)) = a `1 proof let a be Point of (TOP-REAL 2); ::_thesis: lower_bound (proj1 .: (east_halfline a)) = a `1 set X = proj1 .: (east_halfline a); A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj1_.:_(east_halfline_a)_holds_ a_`1_<=_r let r be real number ; ::_thesis: ( r in proj1 .: (east_halfline a) implies a `1 <= r ) assume r in proj1 .: (east_halfline a) ; ::_thesis: a `1 <= r then consider x being set such that A2: x in the carrier of (TOP-REAL 2) and A3: x in east_halfline a and A4: r = proj1 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A2; r = x `1 by A4, PSCOMP_1:def_5; hence a `1 <= r by A3, TOPREAL1:def_11; ::_thesis: verum end; A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r_being_real_number_st_ (_r_in_proj1_.:_(east_halfline_a)_&_r_<_(a_`1)_+_s_) reconsider r = a `1 as real number ; let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in proj1 .: (east_halfline a) & r < (a `1) + s ) ) assume 0 < s ; ::_thesis: ex r being real number st ( r in proj1 .: (east_halfline a) & r < (a `1) + s ) then A6: r + 0 < (a `1) + s by XREAL_1:8; take r = r; ::_thesis: ( r in proj1 .: (east_halfline a) & r < (a `1) + s ) ( a in east_halfline a & r = proj1 . a ) by PSCOMP_1:def_5, TOPREAL1:38; hence r in proj1 .: (east_halfline a) by FUNCT_2:35; ::_thesis: r < (a `1) + s thus r < (a `1) + s by A6; ::_thesis: verum end; proj1 .: (east_halfline a) is bounded_below by Th6; hence lower_bound (proj1 .: (east_halfline a)) = a `1 by A1, A5, SEQ_4:def_2; ::_thesis: verum end; Lm3: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; registration let a be Point of (TOP-REAL 2); cluster north_halfline a -> closed ; coherence north_halfline a is closed proof set X = north_halfline a; reconsider XX = (north_halfline a) ` as Subset of (TOP-REAL 2) ; reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3; for p being Point of (Euclid 2) st p in (north_halfline a) ` holds ex r being real number st ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) proof let p be Point of (Euclid 2); ::_thesis: ( p in (north_halfline a) ` implies ex r being real number st ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) ) reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67; assume p in (north_halfline a) ` ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) then A1: not p in north_halfline a by XBOOLE_0:def_5; percases ( x `1 <> a `1 or x `2 < a `2 ) by A1, TOPREAL1:def_10; supposeA2: x `1 <> a `1 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) take r = abs ((x `1) - (a `1)); ::_thesis: ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) (x `1) - (a `1) <> 0 by A2; hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (north_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (north_halfline a) ` ) assume A3: b in Ball (p,r) ; ::_thesis: b in (north_halfline a) ` then reconsider bb = b as Point of (Euclid 2) ; reconsider c = bb as Point of (TOP-REAL 2) by EUCLID:67; dist (p,bb) < r by A3, METRIC_1:11; then A4: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`1_=_a_`1 assume c `1 = a `1 ; ::_thesis: contradiction then A5: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `1) - (c `1)) by A4, TOPREAL6:92; A6: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; A7: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A6, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `1) - (c `1))) ^2 by A5, SQUARE_1:16; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (c `1)) ^2 by COMPLEX1:75; then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `1) - (c `1)) ^2) + 0 by A6, SQUARE_1:def_2; hence contradiction by A7, XREAL_1:7; ::_thesis: verum end; then not c in north_halfline a by TOPREAL1:def_10; hence b in (north_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; supposeA8: x `2 < a `2 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) take r = (a `2) - (x `2); ::_thesis: ( r > 0 & Ball (p,r) c= (north_halfline a) ` ) thus r > 0 by A8, XREAL_1:50; ::_thesis: Ball (p,r) c= (north_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (north_halfline a) ` ) assume A9: b in Ball (p,r) ; ::_thesis: b in (north_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A9, METRIC_1:11; then A10: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`2_>=_a_`2 assume c `2 >= a `2 ; ::_thesis: contradiction then A11: (a `2) - (x `2) <= (c `2) - (x `2) by XREAL_1:13; 0 <= (a `2) - (x `2) by A8, XREAL_1:50; then A12: ((a `2) - (x `2)) ^2 <= ((c `2) - (x `2)) ^2 by A11, SQUARE_1:15; A13: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; A14: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (a `2) - (x `2) by A10, TOPREAL6:92; A15: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A13, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `2) - (x `2)) ^2 by A14, SQUARE_1:16; then A16: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `2) - (x `2)) ^2 by A13, A15, SQUARE_1:def_2; 0 + (((x `2) - (c `2)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A13, XREAL_1:7; hence contradiction by A16, A12, XXREAL_0:2; ::_thesis: verum end; then not c in north_halfline a by TOPREAL1:def_10; hence b in (north_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; end; end; then OO is open by TOPMETR:15; then XX is open by Lm3, PRE_TOPC:30; then XX ` is closed ; hence north_halfline a is closed ; ::_thesis: verum end; cluster south_halfline a -> closed ; coherence south_halfline a is closed proof set X = south_halfline a; reconsider XX = (south_halfline a) ` as Subset of (TOP-REAL 2) ; reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3; for p being Point of (Euclid 2) st p in (south_halfline a) ` holds ex r being real number st ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) proof let p be Point of (Euclid 2); ::_thesis: ( p in (south_halfline a) ` implies ex r being real number st ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) ) reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67; assume p in (south_halfline a) ` ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) then A17: not p in south_halfline a by XBOOLE_0:def_5; percases ( x `1 <> a `1 or x `2 > a `2 ) by A17, TOPREAL1:def_12; supposeA18: x `1 <> a `1 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) take r = abs ((x `1) - (a `1)); ::_thesis: ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) (x `1) - (a `1) <> 0 by A18; hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (south_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (south_halfline a) ` ) assume A19: b in Ball (p,r) ; ::_thesis: b in (south_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A19, METRIC_1:11; then A20: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`1_=_a_`1 assume c `1 = a `1 ; ::_thesis: contradiction then A21: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `1) - (c `1)) by A20, TOPREAL6:92; A22: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; A23: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A22, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `1) - (c `1))) ^2 by A21, SQUARE_1:16; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (c `1)) ^2 by COMPLEX1:75; then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `1) - (c `1)) ^2) + 0 by A22, SQUARE_1:def_2; hence contradiction by A23, XREAL_1:7; ::_thesis: verum end; then not c in south_halfline a by TOPREAL1:def_12; hence b in (south_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; supposeA24: x `2 > a `2 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) take r = (x `2) - (a `2); ::_thesis: ( r > 0 & Ball (p,r) c= (south_halfline a) ` ) thus r > 0 by A24, XREAL_1:50; ::_thesis: Ball (p,r) c= (south_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (south_halfline a) ` ) assume A25: b in Ball (p,r) ; ::_thesis: b in (south_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A25, METRIC_1:11; then A26: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`2_<=_a_`2 assume c `2 <= a `2 ; ::_thesis: contradiction then A27: (x `2) - (c `2) >= (x `2) - (a `2) by XREAL_1:13; 0 <= (x `2) - (a `2) by A24, XREAL_1:50; then A28: ((x `2) - (a `2)) ^2 <= ((x `2) - (c `2)) ^2 by A27, SQUARE_1:15; A29: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; A30: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (x `2) - (a `2) by A26, TOPREAL6:92; A31: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A29, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (a `2)) ^2 by A30, SQUARE_1:16; then A32: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((x `2) - (a `2)) ^2 by A29, A31, SQUARE_1:def_2; 0 + (((x `2) - (c `2)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A29, XREAL_1:7; hence contradiction by A32, A28, XXREAL_0:2; ::_thesis: verum end; then not c in south_halfline a by TOPREAL1:def_12; hence b in (south_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; end; end; then OO is open by TOPMETR:15; then XX is open by Lm3, PRE_TOPC:30; then XX ` is closed ; hence south_halfline a is closed ; ::_thesis: verum end; cluster east_halfline a -> closed ; coherence east_halfline a is closed proof set X = east_halfline a; reconsider XX = (east_halfline a) ` as Subset of (TOP-REAL 2) ; reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3; for p being Point of (Euclid 2) st p in (east_halfline a) ` holds ex r being real number st ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) proof let p be Point of (Euclid 2); ::_thesis: ( p in (east_halfline a) ` implies ex r being real number st ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) ) reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67; assume p in (east_halfline a) ` ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) then A33: not p in east_halfline a by XBOOLE_0:def_5; percases ( x `2 <> a `2 or x `1 < a `1 ) by A33, TOPREAL1:def_11; supposeA34: x `2 <> a `2 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) take r = abs ((x `2) - (a `2)); ::_thesis: ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) (x `2) - (a `2) <> 0 by A34; hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (east_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (east_halfline a) ` ) assume A35: b in Ball (p,r) ; ::_thesis: b in (east_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A35, METRIC_1:11; then A36: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`2_=_a_`2 assume c `2 = a `2 ; ::_thesis: contradiction then A37: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `2) - (c `2)) by A36, TOPREAL6:92; A38: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; A39: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A38, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `2) - (c `2))) ^2 by A37, SQUARE_1:16; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (c `2)) ^2 by COMPLEX1:75; then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `2) - (c `2)) ^2) + 0 by A38, SQUARE_1:def_2; hence contradiction by A39, XREAL_1:7; ::_thesis: verum end; then not c in east_halfline a by TOPREAL1:def_11; hence b in (east_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; supposeA40: x `1 < a `1 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) take r = (a `1) - (x `1); ::_thesis: ( r > 0 & Ball (p,r) c= (east_halfline a) ` ) thus r > 0 by A40, XREAL_1:50; ::_thesis: Ball (p,r) c= (east_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (east_halfline a) ` ) assume A41: b in Ball (p,r) ; ::_thesis: b in (east_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A41, METRIC_1:11; then A42: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`1_>=_a_`1 assume c `1 >= a `1 ; ::_thesis: contradiction then A43: (a `1) - (x `1) <= (c `1) - (x `1) by XREAL_1:13; 0 <= (a `1) - (x `1) by A40, XREAL_1:50; then A44: ((a `1) - (x `1)) ^2 <= ((c `1) - (x `1)) ^2 by A43, SQUARE_1:15; A45: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; A46: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (a `1) - (x `1) by A42, TOPREAL6:92; A47: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A45, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `1) - (x `1)) ^2 by A46, SQUARE_1:16; then A48: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `1) - (x `1)) ^2 by A45, A47, SQUARE_1:def_2; (((x `1) - (c `1)) ^2) + 0 <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A45, XREAL_1:7; hence contradiction by A48, A44, XXREAL_0:2; ::_thesis: verum end; then not c in east_halfline a by TOPREAL1:def_11; hence b in (east_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; end; end; then OO is open by TOPMETR:15; then XX is open by Lm3, PRE_TOPC:30; then XX ` is closed ; hence east_halfline a is closed ; ::_thesis: verum end; cluster west_halfline a -> closed ; coherence west_halfline a is closed proof set X = west_halfline a; reconsider XX = (west_halfline a) ` as Subset of (TOP-REAL 2) ; reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3; for p being Point of (Euclid 2) st p in (west_halfline a) ` holds ex r being real number st ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) proof let p be Point of (Euclid 2); ::_thesis: ( p in (west_halfline a) ` implies ex r being real number st ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) ) reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67; assume p in (west_halfline a) ` ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) then A49: not p in west_halfline a by XBOOLE_0:def_5; percases ( x `2 <> a `2 or x `1 > a `1 ) by A49, TOPREAL1:def_13; supposeA50: x `2 <> a `2 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) take r = abs ((x `2) - (a `2)); ::_thesis: ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) (x `2) - (a `2) <> 0 by A50; hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (west_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (west_halfline a) ` ) assume A51: b in Ball (p,r) ; ::_thesis: b in (west_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A51, METRIC_1:11; then A52: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`2_=_a_`2 assume c `2 = a `2 ; ::_thesis: contradiction then A53: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `2) - (c `2)) by A52, TOPREAL6:92; A54: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; A55: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A54, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `2) - (c `2))) ^2 by A53, SQUARE_1:16; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (c `2)) ^2 by COMPLEX1:75; then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `2) - (c `2)) ^2) + 0 by A54, SQUARE_1:def_2; hence contradiction by A55, XREAL_1:7; ::_thesis: verum end; then not c in west_halfline a by TOPREAL1:def_13; hence b in (west_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; supposeA56: x `1 > a `1 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) take r = (x `1) - (a `1); ::_thesis: ( r > 0 & Ball (p,r) c= (west_halfline a) ` ) thus r > 0 by A56, XREAL_1:50; ::_thesis: Ball (p,r) c= (west_halfline a) ` let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (west_halfline a) ` ) assume A57: b in Ball (p,r) ; ::_thesis: b in (west_halfline a) ` then reconsider b = b as Point of (Euclid 2) ; reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67; dist (p,b) < r by A57, METRIC_1:11; then A58: dist (x,c) < r by TOPREAL6:def_1; now__::_thesis:_not_c_`1_<=_a_`1 assume c `1 <= a `1 ; ::_thesis: contradiction then A59: (x `1) - (c `1) >= (x `1) - (a `1) by XREAL_1:13; 0 <= (x `1) - (a `1) by A56, XREAL_1:50; then A60: ((x `1) - (a `1)) ^2 <= ((x `1) - (c `1)) ^2 by A59, SQUARE_1:15; A61: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63; A62: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (x `1) - (a `1) by A58, TOPREAL6:92; A63: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63; then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A61, SQUARE_1:def_2; then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (a `1)) ^2 by A62, SQUARE_1:16; then A64: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((x `1) - (a `1)) ^2 by A61, A63, SQUARE_1:def_2; 0 + (((x `1) - (c `1)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A61, XREAL_1:7; hence contradiction by A64, A60, XXREAL_0:2; ::_thesis: verum end; then not c in west_halfline a by TOPREAL1:def_13; hence b in (west_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum end; end; end; then OO is open by TOPMETR:15; then XX is open by Lm3, PRE_TOPC:30; then XX ` is closed ; hence west_halfline a is closed ; ::_thesis: verum end; end; theorem Th11: :: JORDAN18:11 for P being Subset of (TOP-REAL 2) for a being Point of (TOP-REAL 2) st a in BDD P holds not north_halfline a c= UBD P proof let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds not north_halfline a c= UBD P let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not north_halfline a c= UBD P ) A1: ( BDD P misses UBD P & a in north_halfline a ) by JORDAN2C:24, TOPREAL1:38; assume a in BDD P ; ::_thesis: not north_halfline a c= UBD P hence not north_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum end; theorem Th12: :: JORDAN18:12 for P being Subset of (TOP-REAL 2) for a being Point of (TOP-REAL 2) st a in BDD P holds not south_halfline a c= UBD P proof let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds not south_halfline a c= UBD P let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not south_halfline a c= UBD P ) A1: ( BDD P misses UBD P & a in south_halfline a ) by JORDAN2C:24, TOPREAL1:38; assume a in BDD P ; ::_thesis: not south_halfline a c= UBD P hence not south_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum end; theorem :: JORDAN18:13 for P being Subset of (TOP-REAL 2) for a being Point of (TOP-REAL 2) st a in BDD P holds not east_halfline a c= UBD P proof let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds not east_halfline a c= UBD P let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not east_halfline a c= UBD P ) A1: ( BDD P misses UBD P & a in east_halfline a ) by JORDAN2C:24, TOPREAL1:38; assume a in BDD P ; ::_thesis: not east_halfline a c= UBD P hence not east_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum end; theorem :: JORDAN18:14 for P being Subset of (TOP-REAL 2) for a being Point of (TOP-REAL 2) st a in BDD P holds not west_halfline a c= UBD P proof let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds not west_halfline a c= UBD P let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not west_halfline a c= UBD P ) A1: ( BDD P misses UBD P & a in west_halfline a ) by JORDAN2C:24, TOPREAL1:38; assume a in BDD P ; ::_thesis: not west_halfline a c= UBD P hence not west_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum end; theorem Th15: :: JORDAN18:15 for C being Simple_closed_curve 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 & P c= C holds ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) proof let C be Simple_closed_curve; ::_thesis: 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 & P c= C holds ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) 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 & P c= C holds ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & P c= C implies ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) ) assume that A1: P is_an_arc_of p1,p2 and A2: P c= C ; ::_thesis: ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) A3: p1 <> p2 by A1, JORDAN6:37; ( p1 in P & p2 in P ) by A1, TOPREAL1:1; then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that A4: P1 is_an_arc_of p1,p2 and A5: P2 is_an_arc_of p1,p2 and A6: C = P1 \/ P2 and A7: P1 /\ P2 = {p1,p2} by A2, A3, TOPREAL2:5; reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ; A8: ( P1 c= C & P2 c= C ) by A6, XBOOLE_1:7; A9: now__::_thesis:_not_P1_=_P2 assume A10: P1 = P2 ; ::_thesis: contradiction ex p3 being Point of (TOP-REAL 2) st ( p3 in P1 & p3 <> p1 & p3 <> p2 ) by A4, JORDAN6:42; hence contradiction by A7, A10, TARSKI:def_2; ::_thesis: verum end; percases ( P = P1 or P = P2 ) by A1, A2, A4, A5, A8, A9, JORDAN16:14; supposeA11: P = P1 ; ::_thesis: ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) take P2 ; ::_thesis: ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} ) thus ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} ) by A5, A6, A7, A11; ::_thesis: verum end; supposeA12: P = P2 ; ::_thesis: ex R being non empty Subset of (TOP-REAL 2) st ( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) take P1 ; ::_thesis: ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} ) thus ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} ) by A4, A6, A7, A12; ::_thesis: verum end; end; end; begin definition let p be Point of (TOP-REAL 2); let P be Subset of (TOP-REAL 2); func North-Bound (p,P) -> Point of (TOP-REAL 2) equals :: JORDAN18:def 1 |[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]|; correctness coherence |[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]| is Point of (TOP-REAL 2); ; func South-Bound (p,P) -> Point of (TOP-REAL 2) equals :: JORDAN18:def 2 |[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]|; correctness coherence |[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]| is Point of (TOP-REAL 2); ; end; :: deftheorem defines North-Bound JORDAN18:def_1_:_ for p being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) holds North-Bound (p,P) = |[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]|; :: deftheorem defines South-Bound JORDAN18:def_2_:_ for p being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) holds South-Bound (p,P) = |[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]|; theorem :: JORDAN18:16 for P being Subset of (TOP-REAL 2) for p being Point of (TOP-REAL 2) holds ( (North-Bound (p,P)) `1 = p `1 & (South-Bound (p,P)) `1 = p `1 ) by EUCLID:52; theorem Th17: :: JORDAN18:17 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) proof let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) ) set X = C /\ (north_halfline p); C /\ (north_halfline p) c= C by XBOOLE_1:17; then proj2 .: (C /\ (north_halfline p)) is real-bounded by JCT_MISC:14, RLTOPSP1:42; then A1: proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def_11; assume A2: p in BDD C ; ::_thesis: ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) then not north_halfline p c= UBD C by Th11; then north_halfline p meets C by JORDAN2C:129; then A3: not C /\ (north_halfline p) is empty by XBOOLE_0:def_7; C /\ (north_halfline p) is bounded by RLTOPSP1:42, XBOOLE_1:17; then proj2 .: (C /\ (north_halfline p)) is closed by JCT_MISC:13; then lower_bound (proj2 .: (C /\ (north_halfline p))) in proj2 .: (C /\ (north_halfline p)) by A3, A1, Lm2, RCOMP_1:13, RELAT_1:119; then consider x being set such that A4: x in the carrier of (TOP-REAL 2) and A5: x in C /\ (north_halfline p) and A6: lower_bound (proj2 .: (C /\ (north_halfline p))) = proj2 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A4; A7: x `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) by A6, PSCOMP_1:def_6 .= (North-Bound (p,C)) `2 by EUCLID:52 ; x in north_halfline p by A5, XBOOLE_0:def_4; then x `1 = p `1 by TOPREAL1:def_10 .= (North-Bound (p,C)) `1 by EUCLID:52 ; then x = North-Bound (p,C) by A7, TOPREAL3:6; hence ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by A5, XBOOLE_0:def_4; ::_thesis: ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) set X = C /\ (south_halfline p); C /\ (south_halfline p) c= C by XBOOLE_1:17; then proj2 .: (C /\ (south_halfline p)) is real-bounded by JCT_MISC:14, RLTOPSP1:42; then A8: proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def_11; not south_halfline p c= UBD C by A2, Th12; then south_halfline p meets C by JORDAN2C:128; then A9: not C /\ (south_halfline p) is empty by XBOOLE_0:def_7; C /\ (south_halfline p) is bounded by RLTOPSP1:42, XBOOLE_1:17; then proj2 .: (C /\ (south_halfline p)) is closed by JCT_MISC:13; then upper_bound (proj2 .: (C /\ (south_halfline p))) in proj2 .: (C /\ (south_halfline p)) by A9, A8, Lm2, RCOMP_1:12, RELAT_1:119; then consider x being set such that A10: x in the carrier of (TOP-REAL 2) and A11: x in C /\ (south_halfline p) and A12: upper_bound (proj2 .: (C /\ (south_halfline p))) = proj2 . x by FUNCT_2:64; reconsider x = x as Point of (TOP-REAL 2) by A10; x in south_halfline p by A11, XBOOLE_0:def_4; then A13: x `1 = p `1 by TOPREAL1:def_12 .= (South-Bound (p,C)) `1 by EUCLID:52 ; x `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by A12, PSCOMP_1:def_6 .= (South-Bound (p,C)) `2 by EUCLID:52 ; then x = South-Bound (p,C) by A13, TOPREAL3:6; hence ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by A11, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th18: :: JORDAN18:18 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) proof let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) ) assume A1: p in BDD C ; ::_thesis: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) then ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by Th17; then South-Bound (p,C) in C /\ (south_halfline p) by XBOOLE_0:def_4; then A2: not proj2 .: (C /\ (south_halfline p)) is empty by Lm2, RELAT_1:119; A3: BDD C misses C by JORDAN1A:7; A4: now__::_thesis:_not_(South-Bound_(p,C))_`2_=_p_`2 A5: (South-Bound (p,C)) `1 = p `1 by EUCLID:52; assume (South-Bound (p,C)) `2 = p `2 ; ::_thesis: contradiction then South-Bound (p,C) = p by A5, TOPREAL3:6; then p in C by A1, Th17; hence contradiction by A1, A3, XBOOLE_0:3; ::_thesis: verum end; ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by A1, Th17; then not C /\ (north_halfline p) is empty by XBOOLE_0:def_4; then A6: not proj2 .: (C /\ (north_halfline p)) is empty by Lm2, RELAT_1:119; ( proj2 .: (south_halfline p) is bounded_above & C /\ (south_halfline p) c= south_halfline p ) by Th4, XBOOLE_1:17; then A7: upper_bound (proj2 .: (C /\ (south_halfline p))) <= upper_bound (proj2 .: (south_halfline p)) by A2, RELAT_1:123, SEQ_4:48; A8: now__::_thesis:_not_(North-Bound_(p,C))_`2_=_p_`2 A9: (North-Bound (p,C)) `1 = p `1 by EUCLID:52; assume (North-Bound (p,C)) `2 = p `2 ; ::_thesis: contradiction then North-Bound (p,C) = p by A9, TOPREAL3:6; then p in C by A1, Th17; hence contradiction by A1, A3, XBOOLE_0:3; ::_thesis: verum end; ( (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) & upper_bound (proj2 .: (south_halfline p)) = p `2 ) by Th8, EUCLID:52; hence (South-Bound (p,C)) `2 < p `2 by A7, A4, XXREAL_0:1; ::_thesis: p `2 < (North-Bound (p,C)) `2 ( proj2 .: (north_halfline p) is bounded_below & C /\ (north_halfline p) c= north_halfline p ) by Th3, XBOOLE_1:17; then A10: lower_bound (proj2 .: (C /\ (north_halfline p))) >= lower_bound (proj2 .: (north_halfline p)) by A6, RELAT_1:123, SEQ_4:47; ( lower_bound (proj2 .: (north_halfline p)) = p `2 & (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) ) by Th7, EUCLID:52; hence p `2 < (North-Bound (p,C)) `2 by A10, A8, XXREAL_0:1; ::_thesis: verum end; theorem Th19: :: JORDAN18:19 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) proof let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) ) assume p in BDD C ; ::_thesis: lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) then A1: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by Th18; ( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52; hence lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) by A1, XXREAL_0:2; ::_thesis: verum end; theorem :: JORDAN18:20 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds South-Bound (p,C) <> North-Bound (p,C) proof let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds South-Bound (p,C) <> North-Bound (p,C) let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies South-Bound (p,C) <> North-Bound (p,C) ) assume A1: p in BDD C ; ::_thesis: South-Bound (p,C) <> North-Bound (p,C) A2: ( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52; assume not South-Bound (p,C) <> North-Bound (p,C) ; ::_thesis: contradiction hence contradiction by A1, A2, Th19; ::_thesis: verum end; theorem Th21: :: JORDAN18:21 for p being Point of (TOP-REAL 2) for C being Subset of (TOP-REAL 2) holds LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical proof let p be Point of (TOP-REAL 2); ::_thesis: for C being Subset of (TOP-REAL 2) holds LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical let C be Subset of (TOP-REAL 2); ::_thesis: LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical ( (North-Bound (p,C)) `1 = p `1 & (South-Bound (p,C)) `1 = p `1 ) by EUCLID:52; hence LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical by SPPOL_1:16; ::_thesis: verum end; theorem :: JORDAN18:22 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))} proof let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))} let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))} ) set L = LSeg ((North-Bound (p,C)),(South-Bound (p,C))); assume A1: p in BDD C ; ::_thesis: (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))} then A2: ( North-Bound (p,C) in C & South-Bound (p,C) in C ) by Th17; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(North-Bound (p,C)),(South-Bound (p,C))} c= (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C A3: (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) by EUCLID:52; A4: (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by EUCLID:52; let x be set ; ::_thesis: ( x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C implies x in {(North-Bound (p,C)),(South-Bound (p,C))} ) A5: (South-Bound (p,C)) `1 = p `1 by EUCLID:52; assume A6: x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C ; ::_thesis: x in {(North-Bound (p,C)),(South-Bound (p,C))} then reconsider y = x as Point of (TOP-REAL 2) ; A7: x in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) by A6, XBOOLE_0:def_4; ( LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical & South-Bound (p,C) in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) ) by Th21, RLTOPSP1:68; then A8: y `1 = p `1 by A5, A7, SPPOL_1:def_3; A9: x in C by A6, XBOOLE_0:def_4; A10: (North-Bound (p,C)) `1 = p `1 by EUCLID:52; now__::_thesis:_(_y_<>_North-Bound_(p,C)_implies_y_=_South-Bound_(p,C)_) C /\ (north_halfline p) is bounded by TOPREAL6:89; then proj2 .: (C /\ (north_halfline p)) is real-bounded by JCT_MISC:14; then A11: proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def_11; ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by A1, Th18; then A12: (South-Bound (p,C)) `2 < (North-Bound (p,C)) `2 by XXREAL_0:2; then A13: (South-Bound (p,C)) `2 <= y `2 by A7, TOPREAL1:4; assume y <> North-Bound (p,C) ; ::_thesis: y = South-Bound (p,C) then A14: y `2 <> (North-Bound (p,C)) `2 by A10, A8, TOPREAL3:6; A15: y `2 = proj2 . y by PSCOMP_1:def_6; y `2 <= (North-Bound (p,C)) `2 by A7, A12, TOPREAL1:4; then A16: y `2 < (North-Bound (p,C)) `2 by A14, XXREAL_0:1; now__::_thesis:_not_y_`2_>_p_`2 assume y `2 > p `2 ; ::_thesis: contradiction then y in north_halfline p by A8, TOPREAL1:def_10; then y in C /\ (north_halfline p) by A9, XBOOLE_0:def_4; then y `2 in proj2 .: (C /\ (north_halfline p)) by A15, FUNCT_2:35; hence contradiction by A3, A16, A11, SEQ_4:def_2; ::_thesis: verum end; then y in south_halfline p by A8, TOPREAL1:def_12; then y in C /\ (south_halfline p) by A9, XBOOLE_0:def_4; then A17: y `2 in proj2 .: (C /\ (south_halfline p)) by A15, FUNCT_2:35; C /\ (south_halfline p) is bounded by TOPREAL6:89; then proj2 .: (C /\ (south_halfline p)) is real-bounded by JCT_MISC:14; then proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def_11; then y `2 <= (South-Bound (p,C)) `2 by A4, A17, SEQ_4:def_1; then y `2 = (South-Bound (p,C)) `2 by A13, XXREAL_0:1; hence y = South-Bound (p,C) by A5, A8, TOPREAL3:6; ::_thesis: verum end; hence x in {(North-Bound (p,C)),(South-Bound (p,C))} by TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(North-Bound (p,C)),(South-Bound (p,C))} or x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C ) assume x in {(North-Bound (p,C)),(South-Bound (p,C))} ; ::_thesis: x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C then A18: ( x = North-Bound (p,C) or x = South-Bound (p,C) ) by TARSKI:def_2; then x in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) by RLTOPSP1:68; hence x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C by A18, A2, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: JORDAN18:23 for p, q being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C & q in BDD C & p `1 <> q `1 holds North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different proof let p, q be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C & q in BDD C & p `1 <> q `1 holds North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C & q in BDD C & p `1 <> q `1 implies North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different ) set np = North-Bound (p,C); set sq = South-Bound (q,C); set nq = North-Bound (q,C); set sp = South-Bound (p,C); A1: ( (North-Bound (p,C)) `1 = p `1 & (South-Bound (p,C)) `1 = p `1 ) by EUCLID:52; A2: ( (North-Bound (q,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline q))) & (South-Bound (q,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline q))) ) by EUCLID:52; A3: ( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52; assume ( p in BDD C & q in BDD C & p `1 <> q `1 ) ; ::_thesis: North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different hence ( North-Bound (p,C) <> South-Bound (q,C) & North-Bound (p,C) <> North-Bound (q,C) & North-Bound (p,C) <> South-Bound (p,C) & South-Bound (q,C) <> North-Bound (q,C) & South-Bound (q,C) <> South-Bound (p,C) & North-Bound (q,C) <> South-Bound (p,C) ) by A1, A2, A3, Th19, EUCLID:52; :: according to ZFMISC_1:def_6 ::_thesis: verum end; begin definition let n be Element of NAT ; let V be Subset of (TOP-REAL n); let s1, s2, t1, t2 be Point of (TOP-REAL n); preds1,s2,V -separate t1,t2 means :Def3: :: JORDAN18:def 3 for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds A meets {t1,t2}; end; :: deftheorem Def3 defines -separate JORDAN18:def_3_:_ for n being Element of NAT for V being Subset of (TOP-REAL n) for s1, s2, t1, t2 being Point of (TOP-REAL n) holds ( s1,s2,V -separate t1,t2 iff for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds A meets {t1,t2} ); notation let n be Element of NAT ; let V be Subset of (TOP-REAL n); let s1, s2, t1, t2 be Point of (TOP-REAL n); antonym s1,s2 are_neighbours_wrt t1,t2,V for s1,s2,V -separate t1,t2; end; theorem :: JORDAN18:24 for n being Element of NAT for V being Subset of (TOP-REAL n) for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2 proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2 let V be Subset of (TOP-REAL n); ::_thesis: for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2 let t, s1, s2 be Point of (TOP-REAL n); ::_thesis: t,t,V -separate s1,s2 assume not t,t,V -separate s1,s2 ; ::_thesis: contradiction then ex A being Subset of (TOP-REAL n) st ( A is_an_arc_of t,t & A c= V & A misses {s1,s2} ) by Def3; hence contradiction by JORDAN6:37; ::_thesis: verum end; theorem :: JORDAN18:25 for n being Element of NAT for V being Subset of (TOP-REAL n) for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds s2,s1,V -separate t1,t2 proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds s2,s1,V -separate t1,t2 let V be Subset of (TOP-REAL n); ::_thesis: for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds s2,s1,V -separate t1,t2 let s1, s2, t1, t2 be Point of (TOP-REAL n); ::_thesis: ( s1,s2,V -separate t1,t2 implies s2,s1,V -separate t1,t2 ) assume A1: for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds A meets {t1,t2} ; :: according to JORDAN18:def_3 ::_thesis: s2,s1,V -separate t1,t2 let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s2,s1 & A c= V implies A meets {t1,t2} ) assume ( A is_an_arc_of s2,s1 & A c= V ) ; ::_thesis: A meets {t1,t2} hence A meets {t1,t2} by A1, JORDAN5B:14; ::_thesis: verum end; theorem :: JORDAN18:26 for n being Element of NAT for V being Subset of (TOP-REAL n) for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds s1,s2,V -separate t2,t1 proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds s1,s2,V -separate t2,t1 let V be Subset of (TOP-REAL n); ::_thesis: for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds s1,s2,V -separate t2,t1 let s1, s2, t1, t2 be Point of (TOP-REAL n); ::_thesis: ( s1,s2,V -separate t1,t2 implies s1,s2,V -separate t2,t1 ) assume A1: for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds A meets {t1,t2} ; :: according to JORDAN18:def_3 ::_thesis: s1,s2,V -separate t2,t1 let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s1,s2 & A c= V implies A meets {t2,t1} ) thus ( A is_an_arc_of s1,s2 & A c= V implies A meets {t2,t1} ) by A1; ::_thesis: verum end; theorem Th27: :: JORDAN18:27 for n being Element of NAT for V being Subset of (TOP-REAL n) for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate s,t2 proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate s,t2 let V be Subset of (TOP-REAL n); ::_thesis: for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate s,t2 let s, t1, t2 be Point of (TOP-REAL n); ::_thesis: s,t1,V -separate s,t2 let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s,t1 & A c= V implies A meets {s,t2} ) assume that A1: A is_an_arc_of s,t1 and A c= V ; ::_thesis: A meets {s,t2} A2: s in {s,t2} by TARSKI:def_2; s in A by A1, TOPREAL1:1; hence A meets {s,t2} by A2, XBOOLE_0:3; ::_thesis: verum end; theorem Th28: :: JORDAN18:28 for n being Element of NAT for V being Subset of (TOP-REAL n) for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s let V be Subset of (TOP-REAL n); ::_thesis: for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s let t1, s, t2 be Point of (TOP-REAL n); ::_thesis: t1,s,V -separate t2,s let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {t2,s} ) assume that A1: A is_an_arc_of t1,s and A c= V ; ::_thesis: A meets {t2,s} A2: s in {s,t2} by TARSKI:def_2; s in A by A1, TOPREAL1:1; hence A meets {t2,s} by A2, XBOOLE_0:3; ::_thesis: verum end; theorem Th29: :: JORDAN18:29 for n being Element of NAT for V being Subset of (TOP-REAL n) for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate s,t2 proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate s,t2 let V be Subset of (TOP-REAL n); ::_thesis: for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate s,t2 let t1, s, t2 be Point of (TOP-REAL n); ::_thesis: t1,s,V -separate s,t2 let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {s,t2} ) assume that A1: A is_an_arc_of t1,s and A c= V ; ::_thesis: A meets {s,t2} A2: s in {s,t2} by TARSKI:def_2; s in A by A1, TOPREAL1:1; hence A meets {s,t2} by A2, XBOOLE_0:3; ::_thesis: verum end; theorem Th30: :: JORDAN18:30 for n being Element of NAT for V being Subset of (TOP-REAL n) for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate t2,s proof let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n) for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate t2,s let V be Subset of (TOP-REAL n); ::_thesis: for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate t2,s let s, t1, t2 be Point of (TOP-REAL n); ::_thesis: s,t1,V -separate t2,s let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s,t1 & A c= V implies A meets {t2,s} ) assume that A1: A is_an_arc_of s,t1 and A c= V ; ::_thesis: A meets {t2,s} A2: s in {s,t2} by TARSKI:def_2; s in A by A1, TOPREAL1:1; hence A meets {t2,s} by A2, XBOOLE_0:3; ::_thesis: verum end; theorem :: JORDAN18:31 for C being Simple_closed_curve for p1, p2, q being Point of (TOP-REAL 2) st q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q holds p1,p2 are_neighbours_wrt q,q,C proof let C be Simple_closed_curve; ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q holds p1,p2 are_neighbours_wrt q,q,C let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q implies p1,p2 are_neighbours_wrt q,q,C ) assume that A1: q in C and A2: ( p1 in C & p2 in C & p1 <> p2 ) and A3: ( p1 <> q & p2 <> q ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C consider P1, P2 being non empty Subset of (TOP-REAL 2) such that A4: P1 is_an_arc_of p1,p2 and A5: P2 is_an_arc_of p1,p2 and A6: C = P1 \/ P2 and A7: P1 /\ P2 = {p1,p2} by A2, TOPREAL2:5; percases ( ( q in P1 & not q in P2 ) or ( q in P2 & not q in P1 ) or ( q in P1 & q in P2 ) ) by A1, A6, XBOOLE_0:def_3; supposeA8: ( q in P1 & not q in P2 ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C take P2 ; :: according to JORDAN18:def_3 ::_thesis: ( P2 is_an_arc_of p1,p2 & P2 c= C & not P2 meets {q,q} ) thus P2 is_an_arc_of p1,p2 by A5; ::_thesis: ( P2 c= C & not P2 meets {q,q} ) thus P2 c= C by A6, XBOOLE_1:7; ::_thesis: not P2 meets {q,q} thus P2 misses {q,q} by A8, ZFMISC_1:51; ::_thesis: verum end; supposeA9: ( q in P2 & not q in P1 ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C take P1 ; :: according to JORDAN18:def_3 ::_thesis: ( P1 is_an_arc_of p1,p2 & P1 c= C & not P1 meets {q,q} ) thus P1 is_an_arc_of p1,p2 by A4; ::_thesis: ( P1 c= C & not P1 meets {q,q} ) thus P1 c= C by A6, XBOOLE_1:7; ::_thesis: not P1 meets {q,q} thus P1 misses {q,q} by A9, ZFMISC_1:51; ::_thesis: verum end; suppose ( q in P1 & q in P2 ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C then q in P1 /\ P2 by XBOOLE_0:def_4; hence p1,p2 are_neighbours_wrt q,q,C by A3, A7, TARSKI:def_2; ::_thesis: verum end; end; end; theorem :: JORDAN18:32 for C being Simple_closed_curve for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 holds q1,q2,C -separate p1,p2 proof let C be Simple_closed_curve; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 holds q1,q2,C -separate p1,p2 let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 implies q1,q2,C -separate p1,p2 ) assume that A1: p1 <> p2 and A2: p1 in C and A3: p2 in C and A4: p1,p2,C -separate q1,q2 ; ::_thesis: q1,q2,C -separate p1,p2 percases ( q1 = p1 or q2 = p2 or q1 = p2 or p1 = q2 or ( q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1 ) ) ; suppose q1 = p1 ; ::_thesis: q1,q2,C -separate p1,p2 hence q1,q2,C -separate p1,p2 by Th27; ::_thesis: verum end; suppose q2 = p2 ; ::_thesis: q1,q2,C -separate p1,p2 hence q1,q2,C -separate p1,p2 by Th28; ::_thesis: verum end; suppose q1 = p2 ; ::_thesis: q1,q2,C -separate p1,p2 hence q1,q2,C -separate p1,p2 by Th30; ::_thesis: verum end; suppose p1 = q2 ; ::_thesis: q1,q2,C -separate p1,p2 hence q1,q2,C -separate p1,p2 by Th29; ::_thesis: verum end; supposeA5: ( q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1 ) ; ::_thesis: q1,q2,C -separate p1,p2 let A be Subset of (TOP-REAL 2); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of q1,q2 & A c= C implies A meets {p1,p2} ) assume ( A is_an_arc_of q1,q2 & A c= C ) ; ::_thesis: A meets {p1,p2} then consider B being non empty Subset of (TOP-REAL 2) such that A6: B is_an_arc_of q1,q2 and A7: A \/ B = C and A /\ B = {q1,q2} by Th15; assume A8: A misses {p1,p2} ; ::_thesis: contradiction then not p2 in A by ZFMISC_1:49; then A9: p2 in B by A3, A7, XBOOLE_0:def_3; not p1 in A by A8, ZFMISC_1:49; then p1 in B by A2, A7, XBOOLE_0:def_3; then consider P being non empty Subset of (TOP-REAL 2) such that A10: P is_an_arc_of p1,p2 and A11: P c= B and A12: P misses {q1,q2} by A1, A5, A6, A9, JORDAN16:23; B c= C by A7, XBOOLE_1:7; then P c= C by A11, XBOOLE_1:1; hence contradiction by A4, A10, A12, Def3; ::_thesis: verum end; end; end; theorem :: JORDAN18:33 for C being Simple_closed_curve for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C holds p1,q1 are_neighbours_wrt p2,q2,C proof let C be Simple_closed_curve; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C holds p1,q1 are_neighbours_wrt p2,q2,C let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C implies p1,q1 are_neighbours_wrt p2,q2,C ) assume that A1: ( p1 in C & p2 in C ) and A2: q1 in C and A3: p1 <> p2 and A4: q1 <> p1 and A5: q1 <> p2 and A6: ( q2 <> p1 & q2 <> p2 ) ; ::_thesis: ( p1,p2 are_neighbours_wrt q1,q2,C or p1,q1 are_neighbours_wrt p2,q2,C ) consider P, P1 being non empty Subset of (TOP-REAL 2) such that A7: P is_an_arc_of p1,p2 and A8: P1 is_an_arc_of p1,p2 and A9: C = P \/ P1 and A10: P /\ P1 = {p1,p2} by A1, A3, TOPREAL2:5; A11: P c= C by A9, XBOOLE_1:7; assume A12: for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C holds A meets {q1,q2} ; :: according to JORDAN18:def_3 ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C then A13: P meets {q1,q2} by A7, A9, XBOOLE_1:7; A14: P1 c= C by A9, XBOOLE_1:7; percases ( ( q1 in P & not q2 in P ) or ( q2 in P & not q1 in P ) or ( q1 in P & q2 in P ) ) by A13, ZFMISC_1:51; supposethat A15: q1 in P and A16: not q2 in P ; ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C now__::_thesis:_ex_A_being_Element_of_bool_the_carrier_of_(TOP-REAL_2)_st_ (_A_is_an_arc_of_p1,q1_&_A_c=_C_&_A_misses_{p2,q2}_) take A = Segment (P,p1,p2,p1,q1); ::_thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} ) A17: now__::_thesis:_not_p2_in_A A18: A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) } by JORDAN6:26; assume p2 in A ; ::_thesis: contradiction then ex q being Point of (TOP-REAL 2) st ( p2 = q & LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A18; hence contradiction by A5, A7, JORDAN6:55; ::_thesis: verum end; LE p1,q1,P,p1,p2 by A7, A15, JORDAN5C:10; hence A is_an_arc_of p1,q1 by A4, A7, JORDAN16:21; ::_thesis: ( A c= C & A misses {p2,q2} ) A19: A c= P by JORDAN16:2; hence A c= C by A11, XBOOLE_1:1; ::_thesis: A misses {p2,q2} not q2 in A by A16, A19; hence A misses {p2,q2} by A17, ZFMISC_1:51; ::_thesis: verum end; hence p1,q1 are_neighbours_wrt p2,q2,C by Def3; ::_thesis: verum end; supposethat A20: q2 in P and A21: not q1 in P ; ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C now__::_thesis:_ex_A_being_Element_of_bool_the_carrier_of_(TOP-REAL_2)_st_ (_A_is_an_arc_of_p1,q1_&_A_c=_C_&_A_misses_{p2,q2}_) take A = Segment (P1,p1,p2,p1,q1); ::_thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} ) A22: now__::_thesis:_not_p2_in_A A23: A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) } by JORDAN6:26; assume p2 in A ; ::_thesis: contradiction then ex q being Point of (TOP-REAL 2) st ( p2 = q & LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) by A23; hence contradiction by A5, A8, JORDAN6:55; ::_thesis: verum end; q1 in P1 by A2, A9, A21, XBOOLE_0:def_3; then LE p1,q1,P1,p1,p2 by A8, JORDAN5C:10; hence A is_an_arc_of p1,q1 by A4, A8, JORDAN16:21; ::_thesis: ( A c= C & A misses {p2,q2} ) A24: A c= P1 by JORDAN16:2; hence A c= C by A14, XBOOLE_1:1; ::_thesis: A misses {p2,q2} now__::_thesis:_not_q2_in_A assume q2 in A ; ::_thesis: contradiction then q2 in {p1,p2} by A10, A20, A24, XBOOLE_0:def_4; hence contradiction by A6, TARSKI:def_2; ::_thesis: verum end; hence A misses {p2,q2} by A22, ZFMISC_1:51; ::_thesis: verum end; hence p1,q1 are_neighbours_wrt p2,q2,C by Def3; ::_thesis: verum end; supposeA25: ( q1 in P & q2 in P ) ; ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C P1 meets {q1,q2} by A12, A8, A9, XBOOLE_1:7; then ( q1 in P1 or q2 in P1 ) by ZFMISC_1:51; then ( q1 in {p1,p2} or q2 in {p1,p2} ) by A10, A25, XBOOLE_0:def_4; hence p1,q1 are_neighbours_wrt p2,q2,C by A4, A5, A6, TARSKI:def_2; ::_thesis: verum end; end; end;