:: TOPREAL1 semantic presentation begin scheme :: TOPREAL1:sch 1 FraenkelAlt{ F1() -> non empty set , P1[ set ], P2[ set ] } : { v where v is Element of F1() : ( P1[v] or P2[v] ) } = { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } proof set X = { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; set Y = { v1 where v1 is Element of F1() : P1[v1] } ; set Z = { v2 where v2 is Element of F1() : P2[v2] } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__v_where_v_is_Element_of_F1()_:_(_P1[v]_or_P2[v]_)__}__implies_x_in__{__v1_where_v1_is_Element_of_F1()_:_P1[v1]__}__\/__{__v2_where_v2_is_Element_of_F1()_:_P2[v2]__}__)_&_(_x_in__{__v1_where_v1_is_Element_of_F1()_:_P1[v1]__}__\/__{__v2_where_v2_is_Element_of_F1()_:_P2[v2]__}__implies_x_in__{__v_where_v_is_Element_of_F1()_:_(_P1[v]_or_P2[v]_)__}__)_) let x be set ; ::_thesis: ( ( x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } implies x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ) & ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } ) ) thus ( x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } implies x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ) ::_thesis: ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } ) proof assume x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; ::_thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } then consider v being Element of F1() such that A1: x = v and A2: ( P1[v] or P2[v] ) ; percases ( P1[v] or P2[v] ) by A2; suppose P1[v] ; ::_thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } then x in { v1 where v1 is Element of F1() : P1[v1] } by A1; hence x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by XBOOLE_0:def_3; ::_thesis: verum end; suppose P2[v] ; ::_thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } then x in { v2 where v2 is Element of F1() : P2[v2] } by A1; hence x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by XBOOLE_0:def_3; ::_thesis: verum end; end; end; assume A3: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ; ::_thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } percases ( x in { v1 where v1 is Element of F1() : P1[v1] } or x in { v2 where v2 is Element of F1() : P2[v2] } ) by A3, XBOOLE_0:def_3; suppose x in { v1 where v1 is Element of F1() : P1[v1] } ; ::_thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } then ex v being Element of F1() st ( x = v & P1[v] ) ; hence x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; ::_thesis: verum end; suppose x in { v2 where v2 is Element of F1() : P2[v2] } ; ::_thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } then ex v being Element of F1() st ( x = v & P2[v] ) ; hence x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; ::_thesis: verum end; end; end; hence { v where v is Element of F1() : ( P1[v] or P2[v] ) } = { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by TARSKI:1; ::_thesis: verum end; definition let T be TopSpace; let p1, p2 be Point of T; let P be Subset of T; predP is_an_arc_of p1,p2 means :Def1: :: TOPREAL1:def 1 ex f being Function of I[01],(T | P) st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ); end; :: deftheorem Def1 defines is_an_arc_of TOPREAL1:def_1_:_ for T being TopSpace for p1, p2 being Point of T for P being Subset of T holds ( P is_an_arc_of p1,p2 iff ex f being Function of I[01],(T | P) st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) ); theorem Th1: :: TOPREAL1:1 for T being TopSpace for P being Subset of T for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds ( p1 in P & p2 in P ) proof let T be TopSpace; ::_thesis: for P being Subset of T for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds ( p1 in P & p2 in P ) let P be Subset of T; ::_thesis: for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds ( p1 in P & p2 in P ) let p1, p2 be Point of T; ::_thesis: ( P is_an_arc_of p1,p2 implies ( p1 in P & p2 in P ) ) assume P is_an_arc_of p1,p2 ; ::_thesis: ( p1 in P & p2 in P ) then consider f being Function of I[01],(T | P) such that A1: f is being_homeomorphism and A2: f . 0 = p1 and A3: f . 1 = p2 by Def1; A4: dom f = [#] I[01] by A1, TOPS_2:def_5 .= the carrier of I[01] ; 1 in [.0,1.] by XXREAL_1:1; then A5: p2 in rng f by A3, A4, BORSUK_1:40, FUNCT_1:def_3; A6: rng f = [#] (T | P) by A1, TOPS_2:def_5; 0 in [.0,1.] by XXREAL_1:1; then p1 in rng f by A2, A4, BORSUK_1:40, FUNCT_1:def_3; hence ( p1 in P & p2 in P ) by A5, A6, PRE_TOPC:def_5; ::_thesis: verum end; theorem Th2: :: TOPREAL1:2 for T being T_2 TopSpace for P, Q being Subset of T for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds P \/ Q is_an_arc_of p1,q1 proof let T be T_2 TopSpace; ::_thesis: for P, Q being Subset of T for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds P \/ Q is_an_arc_of p1,q1 let P, Q be Subset of T; ::_thesis: for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds P \/ Q is_an_arc_of p1,q1 let p1, p2, q1 be Point of T; ::_thesis: ( P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} implies P \/ Q is_an_arc_of p1,q1 ) assume that A1: P is_an_arc_of p1,p2 and A2: Q is_an_arc_of p2,q1 and A3: P /\ Q = {p2} ; ::_thesis: P \/ Q is_an_arc_of p1,q1 consider f2 being Function of I[01],(T | Q) such that A4: f2 is being_homeomorphism and A5: f2 . 0 = p2 and A6: f2 . 1 = q1 by A2, Def1; consider f1 being Function of I[01],(T | P) such that A7: f1 is being_homeomorphism and A8: f1 . 0 = p1 and A9: f1 . 1 = p2 by A1, Def1; consider h being Function of I[01],(T | (P \/ Q)) such that A10: h is being_homeomorphism and A11: h . 0 = f1 . 0 and A12: h . 1 = f2 . 1 by A3, A7, A9, A4, A5, TOPMETR2:3; take h ; :: according to TOPREAL1:def_1 ::_thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = q1 ) thus ( h is being_homeomorphism & h . 0 = p1 & h . 1 = q1 ) by A8, A6, A10, A11, A12; ::_thesis: verum end; definition func R^2-unit_square -> Subset of (TOP-REAL 2) equals :: TOPREAL1:def 2 ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))); coherence ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is Subset of (TOP-REAL 2) ; end; :: deftheorem defines R^2-unit_square TOPREAL1:def_2_:_ R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))); Lm1: for n being Nat for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds LSeg (p1,p) c= LSeg (p1,p2) proof let n be Nat; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds LSeg (p1,p) c= LSeg (p1,p2) let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p) c= LSeg (p1,p2) ) assume p in LSeg (p1,p2) ; ::_thesis: LSeg (p1,p) c= LSeg (p1,p2) then consider r being Real such that A1: p = ((1 - r) * p1) + (r * p2) and A2: 0 <= r and A3: r <= 1 ; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in LSeg (p1,p) or q in LSeg (p1,p2) ) assume q in LSeg (p1,p) ; ::_thesis: q in LSeg (p1,p2) then consider b being Real such that A4: q = ((1 - b) * p1) + (b * p) and A5: 0 <= b and A6: b <= 1 ; A7: q = ((1 - b) * p1) + ((b * ((1 - r) * p1)) + (b * (r * p2))) by A1, A4, EUCLID:32 .= (((1 - b) * p1) + (b * ((1 - r) * p1))) + (b * (r * p2)) by EUCLID:26 .= (((1 - b) * p1) + ((b * (1 - r)) * p1)) + (b * (r * p2)) by EUCLID:30 .= (((1 - b) + (b * (1 - r))) * p1) + (b * (r * p2)) by EUCLID:33 .= ((1 - (b * r)) * p1) + ((b * r) * p2) by EUCLID:30 ; b * r <= 1 by A2, A3, A6, XREAL_1:160; hence q in LSeg (p1,p2) by A2, A5, A7; ::_thesis: verum end; theorem :: TOPREAL1:3 for p1, p2, p being Point of (TOP-REAL 2) st p1 `1 <= p2 `1 & p in LSeg (p1,p2) holds ( p1 `1 <= p `1 & p `1 <= p2 `1 ) proof let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: ( p1 `1 <= p2 `1 & p in LSeg (p1,p2) implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) ) assume that A1: p1 `1 <= p2 `1 and A2: p in LSeg (p1,p2) ; ::_thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 ) consider lambda being Real such that A3: p = ((1 - lambda) * p1) + (lambda * p2) and A4: 0 <= lambda and A5: lambda <= 1 by A2; A6: ((1 - lambda) * p1) `1 = |[((1 - lambda) * (p1 `1)),((1 - lambda) * (p1 `2))]| `1 by EUCLID:57 .= (1 - lambda) * (p1 `1) by EUCLID:52 ; A7: (lambda * p2) `1 = |[(lambda * (p2 `1)),(lambda * (p2 `2))]| `1 by EUCLID:57 .= lambda * (p2 `1) by EUCLID:52 ; A8: p `1 = |[((((1 - lambda) * p1) `1) + ((lambda * p2) `1)),((((1 - lambda) * p1) `2) + ((lambda * p2) `2))]| `1 by A3, EUCLID:55 .= ((1 - lambda) * (p1 `1)) + (lambda * (p2 `1)) by A6, A7, EUCLID:52 ; lambda * (p1 `1) <= lambda * (p2 `1) by A1, A4, XREAL_1:64; then ((1 - lambda) * (p1 `1)) + (lambda * (p1 `1)) <= p `1 by A8, XREAL_1:7; hence p1 `1 <= p `1 ; ::_thesis: p `1 <= p2 `1 0 <= 1 - lambda by A5, XREAL_1:48; then (1 - lambda) * (p1 `1) <= (1 - lambda) * (p2 `1) by A1, XREAL_1:64; then p `1 <= ((1 - lambda) * (p2 `1)) + (lambda * (p2 `1)) by A8, XREAL_1:6; hence p `1 <= p2 `1 ; ::_thesis: verum end; theorem :: TOPREAL1:4 for p1, p2, p being Point of (TOP-REAL 2) st p1 `2 <= p2 `2 & p in LSeg (p1,p2) holds ( p1 `2 <= p `2 & p `2 <= p2 `2 ) proof let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: ( p1 `2 <= p2 `2 & p in LSeg (p1,p2) implies ( p1 `2 <= p `2 & p `2 <= p2 `2 ) ) assume that A1: p1 `2 <= p2 `2 and A2: p in LSeg (p1,p2) ; ::_thesis: ( p1 `2 <= p `2 & p `2 <= p2 `2 ) consider lambda being Real such that A3: p = ((1 - lambda) * p1) + (lambda * p2) and A4: 0 <= lambda and A5: lambda <= 1 by A2; A6: ((1 - lambda) * p1) `2 = |[((1 - lambda) * (p1 `1)),((1 - lambda) * (p1 `2))]| `2 by EUCLID:57 .= (1 - lambda) * (p1 `2) by EUCLID:52 ; A7: (lambda * p2) `2 = |[(lambda * (p2 `1)),(lambda * (p2 `2))]| `2 by EUCLID:57 .= lambda * (p2 `2) by EUCLID:52 ; A8: p `2 = |[((((1 - lambda) * p1) `1) + ((lambda * p2) `1)),((((1 - lambda) * p1) `2) + ((lambda * p2) `2))]| `2 by A3, EUCLID:55 .= ((1 - lambda) * (p1 `2)) + (lambda * (p2 `2)) by A6, A7, EUCLID:52 ; lambda * (p1 `2) <= lambda * (p2 `2) by A1, A4, XREAL_1:64; then ((1 - lambda) * (p1 `2)) + (lambda * (p1 `2)) <= p `2 by A8, XREAL_1:7; hence p1 `2 <= p `2 ; ::_thesis: p `2 <= p2 `2 0 <= 1 - lambda by A5, XREAL_1:48; then (1 - lambda) * (p1 `2) <= (1 - lambda) * (p2 `2) by A1, XREAL_1:64; then p `2 <= ((1 - lambda) * (p2 `2)) + (lambda * (p2 `2)) by A8, XREAL_1:6; hence p `2 <= p2 `2 ; ::_thesis: verum end; theorem Th5: :: TOPREAL1:5 for n being Nat for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) proof let n be Nat; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) now__::_thesis:_(_p_in_LSeg_(p1,p2)_&_p_in_LSeg_(p1,p2)_implies_LSeg_(p1,p2)_=_(LSeg_(p1,p))_\/_(LSeg_(p,p2))_) assume A1: p in LSeg (p1,p2) ; ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) then consider r being Real such that A2: p = ((1 - r) * p1) + (r * p2) and A3: 0 <= r and A4: r <= 1 ; now__::_thesis:_(_p_in_LSeg_(p1,p2)_implies_LSeg_(p1,p2)_=_(LSeg_(p1,p))_\/_(LSeg_(p,p2))_) percases ( ( 0 <> r & r <> 1 ) or not 0 <> r or not r <> 1 ) ; supposeA5: ( 0 <> r & r <> 1 ) ; ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) now__::_thesis:_for_q_being_set_st_q_in_LSeg_(p1,p2)_holds_ q_in_(LSeg_(p1,p))_\/_(LSeg_(p,p2)) let q be set ; ::_thesis: ( q in LSeg (p1,p2) implies q in (LSeg (p1,p)) \/ (LSeg (p,p2)) ) assume q in LSeg (p1,p2) ; ::_thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2)) then consider b being Real such that A6: q = ((1 - b) * p1) + (b * p2) and A7: 0 <= b and A8: b <= 1 ; now__::_thesis:_q_in_(LSeg_(p1,p))_\/_(LSeg_(p,p2)) percases ( b <= r or not b <= r ) ; supposeA9: b <= r ; ::_thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2)) set x = b * (1 / r); b * (1 / r) <= r * (1 / r) by A3, A9, XREAL_1:64; then A10: b * (1 / r) <= 1 by A5, XCMPLX_1:106; ((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * p) = ((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * ((1 - r) * p1)) + ((b * (1 / r)) * (r * p2))) by A2, EUCLID:32 .= (((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * ((1 - r) * p1))) + ((b * (1 / r)) * (r * p2)) by EUCLID:26 .= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + ((b * (1 / r)) * (r * p2)) by EUCLID:30 .= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + (((b * (1 / r)) * r) * p2) by EUCLID:30 .= (((1 - (b * (1 / r))) + ((b * (1 / r)) * (1 - r))) * p1) + (((b * (1 / r)) * r) * p2) by EUCLID:33 .= ((1 - ((b * (1 / r)) * r)) * p1) + (b * p2) by A5, XCMPLX_1:109 .= q by A5, A6, XCMPLX_1:109 ; then q in { (((1 - lambda) * p1) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A3, A7, A10; hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) by XBOOLE_0:def_3; ::_thesis: verum end; supposeA11: not b <= r ; ::_thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2)) set bp = 1 - b; set rp = 1 - r; set x = (1 - b) * (1 / (1 - r)); A12: 0 <> 1 - r by A5; r - r = 0 ; then A13: 0 <= 1 - r by A4, XREAL_1:9; 1 - b <= 1 - r by A11, XREAL_1:10; then (1 - b) * (1 / (1 - r)) <= (1 - r) * (1 / (1 - r)) by A13, XREAL_1:64; then A14: (1 - b) * (1 / (1 - r)) <= 1 by A12, XCMPLX_1:106; A15: 0 <= 1 - b by A8, XREAL_1:48; A16: 1 - 0 = 1 ; ((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * p) = ((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1))) by A2, EUCLID:32 .= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2))) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by EUCLID:26 .= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by EUCLID:30 .= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by EUCLID:30 .= (((1 - ((1 - b) * (1 / (1 - r)))) + (((1 - b) * (1 / (1 - r))) * (1 - (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by EUCLID:33 .= ((1 - (((1 - b) * (1 / (1 - r))) * (1 - r))) * p2) + ((1 - b) * p1) by A5, A16, XCMPLX_1:109 .= ((1 - (1 - b)) * p2) + ((1 - b) * p1) by A12, XCMPLX_1:109 .= q by A6 ; then q in { (((1 - lambda) * p2) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A15, A13, A14; then q in LSeg (p,p2) by RLTOPSP1:def_2; hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) ; ::_thesis: verum end; then A17: LSeg (p1,p2) c= (LSeg (p1,p)) \/ (LSeg (p,p2)) by TARSKI:def_3; A18: LSeg (p,p2) c= LSeg (p1,p2) by A1, Lm1; LSeg (p1,p) c= LSeg (p1,p2) by A1, Lm1; then (LSeg (p1,p)) \/ (LSeg (p,p2)) c= LSeg (p1,p2) by A18, XBOOLE_1:8; hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) by A17, XBOOLE_0:def_10; ::_thesis: verum end; supposeA19: ( not 0 <> r or not r <> 1 ) ; ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) now__::_thesis:_LSeg_(p1,p2)_=_(LSeg_(p1,p))_\/_(LSeg_(p,p2)) percases ( r = 0 or r = 1 ) by A19; supposeA20: r = 0 ; ::_thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) A21: p in LSeg (p,p2) by RLTOPSP1:68; A22: p = (1 * p1) + (0. (TOP-REAL n)) by A2, A20, EUCLID:29 .= p1 + (0. (TOP-REAL n)) by EUCLID:29 .= p1 by EUCLID:27 ; then LSeg (p1,p) = {p} by RLTOPSP1:70; then LSeg (p1,p) c= LSeg (p,p2) by A21, ZFMISC_1:31; hence LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A22, XBOOLE_1:12; ::_thesis: verum end; supposeA23: r = 1 ; ::_thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) A24: p in LSeg (p1,p) by RLTOPSP1:68; A25: p = (0. (TOP-REAL n)) + (1 * p2) by A2, A23, EUCLID:29 .= (0. (TOP-REAL n)) + p2 by EUCLID:29 .= p2 by EUCLID:27 ; then LSeg (p,p2) = {p} by RLTOPSP1:70; then LSeg (p,p2) c= LSeg (p1,p) by A24, ZFMISC_1:31; hence LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A25, XBOOLE_1:12; ::_thesis: verum end; end; end; hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; ::_thesis: verum end; end; end; hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; ::_thesis: verum end; hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; ::_thesis: verum end; theorem Th6: :: TOPREAL1:6 for n being Nat for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds LSeg (q1,q2) c= LSeg (p1,p2) proof let n be Nat; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds LSeg (q1,q2) c= LSeg (p1,p2) let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) implies LSeg (q1,q2) c= LSeg (p1,p2) ) assume that A1: q1 in LSeg (p1,p2) and A2: q2 in LSeg (p1,p2) ; ::_thesis: LSeg (q1,q2) c= LSeg (p1,p2) A3: LSeg (p1,p2) = (LSeg (p1,q1)) \/ (LSeg (q1,p2)) by A1, Th5; now__::_thesis:_LSeg_(q1,q2)_c=_LSeg_(p1,p2) percases ( q2 in LSeg (p1,q1) or q2 in LSeg (q1,p2) ) by A2, A3, XBOOLE_0:def_3; supposeA4: q2 in LSeg (p1,q1) ; ::_thesis: LSeg (q1,q2) c= LSeg (p1,p2) A5: LSeg (p1,q1) c= LSeg (p1,p2) by A1, Lm1; LSeg (q2,q1) c= LSeg (p1,q1) by A4, Lm1; hence LSeg (q1,q2) c= LSeg (p1,p2) by A5, XBOOLE_1:1; ::_thesis: verum end; supposeA6: q2 in LSeg (q1,p2) ; ::_thesis: LSeg (q1,q2) c= LSeg (p1,p2) A7: LSeg (q1,p2) c= LSeg (p1,p2) by A1, Lm1; LSeg (q1,q2) c= LSeg (q1,p2) by A6, Lm1; hence LSeg (q1,q2) c= LSeg (p1,p2) by A7, XBOOLE_1:1; ::_thesis: verum end; end; end; hence LSeg (q1,q2) c= LSeg (p1,p2) ; ::_thesis: verum end; theorem :: TOPREAL1:7 for n being Nat for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) proof let n be Nat; ::_thesis: for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) let p, q, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) & q in LSeg (p1,p2) implies LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) ) assume that A1: p in LSeg (p1,p2) and A2: q in LSeg (p1,p2) ; ::_thesis: LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) A3: LSeg (p,q) c= LSeg (p1,p2) by A1, A2, Th6; A4: LSeg (p1,p2) = (LSeg (p1,q)) \/ (LSeg (q,p2)) by A2, Th5; A5: now__::_thesis:_LSeg_(p1,p2)_c=_((LSeg_(p1,p))_\/_(LSeg_(p,q)))_\/_(LSeg_(q,p2)) percases ( p in LSeg (p1,q) or not p in LSeg (p1,q) ) ; suppose p in LSeg (p1,q) ; ::_thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) hence LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A4, Th5; ::_thesis: verum end; suppose not p in LSeg (p1,q) ; ::_thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) then p in LSeg (q,p2) by A1, A4, XBOOLE_0:def_3; then A6: LSeg (q,p2) = (LSeg (q,p)) \/ (LSeg (p,p2)) by Th5; LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A1, Th5; then A7: LSeg (p1,p2) c= (LSeg (p1,p)) \/ (LSeg (q,p2)) by A6, XBOOLE_1:7, XBOOLE_1:9; A8: ((LSeg (p1,p)) \/ (LSeg (q,p2))) \/ (LSeg (p,q)) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by XBOOLE_1:4; (LSeg (p1,p)) \/ (LSeg (q,p2)) c= ((LSeg (p1,p)) \/ (LSeg (q,p2))) \/ (LSeg (p,q)) by XBOOLE_1:7; hence LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A7, A8, XBOOLE_1:1; ::_thesis: verum end; end; end; p1 in LSeg (p1,p2) by RLTOPSP1:68; then LSeg (p1,p) c= LSeg (p1,p2) by A1, Th6; then A9: (LSeg (p1,p)) \/ (LSeg (p,q)) c= LSeg (p1,p2) by A3, XBOOLE_1:8; p2 in LSeg (p1,p2) by RLTOPSP1:68; then LSeg (q,p2) c= LSeg (p1,p2) by A2, Th6; then ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) c= LSeg (p1,p2) by A9, XBOOLE_1:8; hence LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TOPREAL1:8 for n being Nat for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} proof let n be Nat; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) implies (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} ) A1: p in LSeg (p,p2) by RLTOPSP1:68; assume A2: p in LSeg (p1,p2) ; ::_thesis: (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} A3: now__::_thesis:_(LSeg_(p1,p))_/\_(LSeg_(p,p2))_c=_{p} assume not (LSeg (p1,p)) /\ (LSeg (p,p2)) c= {p} ; ::_thesis: contradiction then consider y being set such that A4: y in (LSeg (p1,p)) /\ (LSeg (p,p2)) and A5: not y in {p} by TARSKI:def_3; reconsider q = y as Point of (TOP-REAL n) by A4; A6: q in LSeg (p1,p) by A4, XBOOLE_0:def_4; then consider d being Real such that A7: q = ((1 - d) * p1) + (d * p) and 0 <= d and A8: d <= 1 ; q in LSeg (p,p2) by A4, XBOOLE_0:def_4; then consider e being Real such that A9: q = ((1 - e) * p) + (e * p2) and A10: 0 <= e and e <= 1 ; consider a being Real such that A11: p = ((1 - a) * p1) + (a * p2) and A12: 0 <= a and A13: a <= 1 by A2; A14: 1 - a >= 0 by A13, XREAL_1:48; now__::_thesis:_not_d_=_1 assume d = 1 ; ::_thesis: contradiction then q = ((1 - 1) * p1) + p by A7, EUCLID:29 .= (0. (TOP-REAL n)) + p by EUCLID:29 .= p by EUCLID:27 ; hence contradiction by A5, TARSKI:def_1; ::_thesis: verum end; then d < 1 by A8, XXREAL_0:1; then A15: 1 - d > 0 by XREAL_1:50; now__::_thesis:_not_a_=_0 assume a = 0 ; ::_thesis: contradiction then p = ((1 - 0) * p1) + (0. (TOP-REAL n)) by A11, EUCLID:29 .= (1 - 0) * p1 by EUCLID:27 .= p1 by EUCLID:29 ; hence contradiction by A5, A6, RLTOPSP1:70; ::_thesis: verum end; then A16: (1 - d) * a > 0 by A12, A15, XREAL_1:129; set f = ((1 - e) * a) + e; q = (((1 - e) * ((1 - a) * p1)) + ((1 - e) * (a * p2))) + (e * p2) by A11, A9, EUCLID:32 .= ((((1 - e) * (1 - a)) * p1) + ((1 - e) * (a * p2))) + (e * p2) by EUCLID:30 .= ((((1 - e) * (1 - a)) * p1) + (((1 - e) * a) * p2)) + (e * p2) by EUCLID:30 .= (((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) * p2) + (e * p2)) by EUCLID:26 .= (((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) + e) * p2) by EUCLID:33 ; then A17: p - q = ((((1 - a) * p1) + (a * p2)) - ((1 - (((1 - e) * a) + e)) * p1)) - ((((1 - e) * a) + e) * p2) by A11, EUCLID:46 .= ((((1 - a) * p1) - ((1 - (((1 - e) * a) + e)) * p1)) + (a * p2)) - ((((1 - e) * a) + e) * p2) by EUCLID:45 .= ((((1 - a) - (1 - (((1 - e) * a) + e))) * p1) + (a * p2)) - ((((1 - e) * a) + e) * p2) by EUCLID:50 .= ((((((1 - e) * a) + e) - a) * p1) - ((((1 - e) * a) + e) * p2)) + (a * p2) by EUCLID:45 .= (((((1 - e) * a) + e) - a) * p1) - (((((1 - e) * a) + e) * p2) - (a * p2)) by EUCLID:47 .= (((((1 - e) * a) + e) - a) * p1) - (((((1 - e) * a) + e) - a) * p2) by EUCLID:50 .= ((((1 - e) * a) + e) - a) * (p1 - p2) by EUCLID:49 ; q = ((1 - d) * p1) + ((d * ((1 - a) * p1)) + (d * (a * p2))) by A11, A7, EUCLID:32 .= (((1 - d) * p1) + (d * ((1 - a) * p1))) + (d * (a * p2)) by EUCLID:26 .= (((1 - d) * p1) + ((d * (1 - a)) * p1)) + (d * (a * p2)) by EUCLID:30 .= (((1 - d) + (d * (1 - a))) * p1) + (d * (a * p2)) by EUCLID:33 .= ((1 - (d * a)) * p1) + ((d * a) * p2) by EUCLID:30 ; then p - q = ((((1 - a) * p1) + (a * p2)) - ((1 - (d * a)) * p1)) - ((d * a) * p2) by A11, EUCLID:46 .= ((((1 - a) * p1) - ((1 - (d * a)) * p1)) + (a * p2)) - ((d * a) * p2) by EUCLID:45 .= ((((1 - a) - (1 - (d * a))) * p1) + (a * p2)) - ((d * a) * p2) by EUCLID:50 .= ((((d * a) - a) * p1) - ((d * a) * p2)) + (a * p2) by EUCLID:45 .= (((d * a) - a) * p1) - (((d * a) * p2) - (a * p2)) by EUCLID:47 .= (((d * a) - a) * p1) - (((d * a) - a) * p2) by EUCLID:50 .= ((d * a) - a) * (p1 - p2) by EUCLID:49 ; then (((((1 - e) * a) + e) - a) * (p1 - p2)) - (((d * a) - a) * (p1 - p2)) = 0. (TOP-REAL n) by A17, EUCLID:42; then (((((1 - e) * a) + e) - a) - ((d * a) - a)) * (p1 - p2) = 0. (TOP-REAL n) by EUCLID:50; then A18: ( (((1 - e) * a) + e) - (d * a) = 0 or p1 - p2 = 0. (TOP-REAL n) ) by EUCLID:31; (((1 - e) * a) + e) - (d * a) = ((1 - d) * a) + (e * (1 - a)) ; then p1 = p2 by A10, A18, A16, A14, EUCLID:43; then p in {p1} by A2, RLTOPSP1:70; then p = p1 by TARSKI:def_1; hence contradiction by A5, A6, RLTOPSP1:70; ::_thesis: verum end; p in LSeg (p1,p) by RLTOPSP1:68; then p in (LSeg (p1,p)) /\ (LSeg (p,p2)) by A1, XBOOLE_0:def_4; then {p} c= (LSeg (p1,p)) /\ (LSeg (p,p2)) by ZFMISC_1:31; hence (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} by A3, XBOOLE_0:def_10; ::_thesis: verum end; Lm2: for T being TopSpace holds ( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 ) proof let T be TopSpace; ::_thesis: ( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 ) thus ( T is T_2 implies TopStruct(# the carrier of T, the topology of T #) is T_2 ) ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is T_2 implies T is T_2 ) proof assume A1: T is T_2 ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is T_2 let p, q be Point of TopStruct(# the carrier of T, the topology of T #); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) reconsider pp = p, qq = q as Point of T ; consider G1, G2 being Subset of T such that A3: G1 is open and A4: G2 is open and A5: pp in G1 and A6: qq in G2 and A7: G1 misses G2 by A1, A2, PRE_TOPC:def_10; reconsider H1 = G1, H2 = G2 as Subset of TopStruct(# the carrier of T, the topology of T #) ; take H1 ; ::_thesis: ex b1 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st ( H1 is open & b1 is open & p in H1 & q in b1 & H1 misses b1 ) take H2 ; ::_thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 ) thus ( H1 is open & H2 is open ) by A3, A4, PRE_TOPC:30; ::_thesis: ( p in H1 & q in H2 & H1 misses H2 ) thus ( p in H1 & q in H2 & H1 misses H2 ) by A5, A6, A7; ::_thesis: verum end; assume A8: TopStruct(# the carrier of T, the topology of T #) is T_2 ; ::_thesis: T is T_2 let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of T) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A9: p <> q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of T) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) reconsider pp = p, qq = q as Point of TopStruct(# the carrier of T, the topology of T #) ; consider G1, G2 being Subset of TopStruct(# the carrier of T, the topology of T #) such that A10: G1 is open and A11: G2 is open and A12: pp in G1 and A13: qq in G2 and A14: G1 misses G2 by A8, A9, PRE_TOPC:def_10; reconsider H1 = G1, H2 = G2 as Subset of T ; take H1 ; ::_thesis: ex b1 being Element of K10( the carrier of T) st ( H1 is open & b1 is open & p in H1 & q in b1 & H1 misses b1 ) take H2 ; ::_thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 ) thus ( H1 is open & H2 is open ) by A10, A11, PRE_TOPC:30; ::_thesis: ( p in H1 & q in H2 & H1 misses H2 ) thus ( p in H1 & q in H2 & H1 misses H2 ) by A12, A13, A14; ::_thesis: verum end; registration let n be Nat; cluster the carrier of (TOP-REAL n) -> functional ; coherence the carrier of (TOP-REAL n) is functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in the carrier of (TOP-REAL n) or x is set ) thus ( not x in the carrier of (TOP-REAL n) or x is set ) by EUCLID:23; ::_thesis: verum end; end; theorem Th9: :: TOPREAL1:9 for n being Nat for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds LSeg (p1,p2) is_an_arc_of p1,p2 proof let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds LSeg (p1,p2) is_an_arc_of p1,p2 let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 <> p2 implies LSeg (p1,p2) is_an_arc_of p1,p2 ) set P = LSeg (p1,p2); reconsider PP = LSeg (p1,p2) as Subset of (Euclid n) by EUCLID:67; not PP is empty ; then reconsider PP = LSeg (p1,p2) as non empty Subset of (Euclid n) ; reconsider p19 = p1, p29 = p2 as Element of REAL n by EUCLID:22; defpred S1[ set , set ] means for x being Real st x = $1 holds $2 = ((1 - x) * p1) + (x * p2); A1: [#] I[01] = [.0,1.] by BORSUK_1:40; A2: for a being set st a in [.0,1.] holds ex u being set st S1[a,u] proof let a be set ; ::_thesis: ( a in [.0,1.] implies ex u being set st S1[a,u] ) assume a in [.0,1.] ; ::_thesis: ex u being set st S1[a,u] then reconsider x = a as Real ; take ((1 - x) * p1) + (x * p2) ; ::_thesis: S1[a,((1 - x) * p1) + (x * p2)] thus S1[a,((1 - x) * p1) + (x * p2)] ; ::_thesis: verum end; consider f being Function such that A3: dom f = [.0,1.] and A4: for a being set st a in [.0,1.] holds S1[a,f . a] from CLASSES1:sch_1(A2); A5: rng f c= the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ) assume y in rng f ; ::_thesis: y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) then consider x being set such that A6: x in dom f and A7: y = f . x by FUNCT_1:def_3; x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, A6, RCOMP_1:def_1; then consider r being Real such that A8: r = x and A9: 0 <= r and A10: r <= 1 ; y = ((1 - r) * p1) + (r * p2) by A3, A4, A6, A7, A8; then y in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A9, A10; then y in [#] ((TOP-REAL n) | (LSeg (p1,p2))) by PRE_TOPC:def_5; hence y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: verum end; then reconsider f = f as Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) by A3, BORSUK_1:40, FUNCT_2:def_1, RELSET_1:4; A11: I[01] is compact by HEINE:4, TOPMETR:20; assume A12: p1 <> p2 ; ::_thesis: LSeg (p1,p2) is_an_arc_of p1,p2 now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A13: x1 in dom f and A14: x2 in dom f and A15: f . x1 = f . x2 ; ::_thesis: x1 = x2 x2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, A14, RCOMP_1:def_1; then consider r2 being Real such that A16: r2 = x2 and 0 <= r2 and r2 <= 1 ; A17: f . x2 = ((1 - r2) * p1) + (r2 * p2) by A3, A4, A14, A16; x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, A13, RCOMP_1:def_1; then consider r1 being Real such that A18: r1 = x1 and 0 <= r1 and r1 <= 1 ; f . x1 = ((1 - r1) * p1) + (r1 * p2) by A3, A4, A13, A18; then (((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 * p2) + ((- r1) * p2)) by A15, A17, EUCLID:26; then (((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 + (- r1)) * p2) by EUCLID:33; then ((1 - r1) * p1) + ((r1 * p2) + ((- r1) * p2)) = ((1 - r2) * p1) + ((r2 - r1) * p2) by EUCLID:26; then ((1 - r1) * p1) + ((r1 + (- r1)) * p2) = ((1 - r2) * p1) + ((r2 - r1) * p2) by EUCLID:33; then ((1 - r1) * p1) + (0. (TOP-REAL n)) = ((1 - r2) * p1) + ((r2 - r1) * p2) by EUCLID:29; then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = ((- (1 - r2)) * p1) + (((1 - r2) * p1) + ((r2 - r1) * p2)) by EUCLID:27; then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) * p1) + ((1 - r2) * p1)) + ((r2 - r1) * p2) by EUCLID:26; then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) + (1 - r2)) * p1) + ((r2 - r1) * p2) by EUCLID:33; then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (0. (TOP-REAL n)) + ((r2 - r1) * p2) by EUCLID:29; then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (r2 - r1) * p2 by EUCLID:27; then ((r2 - 1) + (1 - r1)) * p1 = (r2 - r1) * p2 by EUCLID:33; then r2 - r1 = 0 by A12, EUCLID:34; hence x1 = x2 by A18, A16; ::_thesis: verum end; then A19: f is one-to-one by FUNCT_1:def_4; [#] ((TOP-REAL n) | (LSeg (p1,p2))) c= rng f proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) or a in rng f ) assume a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: a in rng f then a in LSeg (p1,p2) by PRE_TOPC:def_5; then consider lambda being Real such that A20: a = ((1 - lambda) * p1) + (lambda * p2) and A21: 0 <= lambda and A22: lambda <= 1 ; lambda in { r where r is Real : ( 0 <= r & r <= 1 ) } by A21, A22; then A23: lambda in dom f by A3, RCOMP_1:def_1; then a = f . lambda by A3, A4, A20; hence a in rng f by A23, FUNCT_1:def_3; ::_thesis: verum end; then A24: rng f = [#] ((TOP-REAL n) | (LSeg (p1,p2))) by A5, XBOOLE_0:def_10; A25: TopSpaceMetr (Euclid n) is T_2 by PCOMPS_1:34; A26: (TOP-REAL n) | (LSeg (p1,p2)) = TopSpaceMetr ((Euclid n) | PP) by EUCLID:63; for W being Point of I[01] for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G proof reconsider p11 = p1, p22 = p2 as Point of (Euclid n) by EUCLID:67; let W be Point of I[01]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G reconsider W9 = W as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10; A27: (Pitag_dist n) . (p19,p29) = dist (p11,p22) by METRIC_1:def_1; [#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5; then reconsider Y = f . W as Point of ((Euclid n) | PP) by TOPMETR:def_2; A28: dist (p11,p22) >= 0 by METRIC_1:5; reconsider W1 = W as Real by BORSUK_1:40, TARSKI:def_3; LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2; then reconsider WW9 = Y as Point of (Euclid n) by TARSKI:def_3; f . W in Int G by CONNSP_2:def_1; then consider Q being Subset of ((TOP-REAL n) | (LSeg (p1,p2))) such that A29: Q is open and A30: Q c= G and A31: f . W in Q by TOPS_1:22; consider r being real number such that A32: r > 0 and A33: Ball (Y,r) c= Q by A26, A29, A31, TOPMETR:15; reconsider r = r as Element of REAL by XREAL_0:def_1; set delta = r / ((Pitag_dist n) . (p19,p29)); reconsider H = Ball (W9,(r / ((Pitag_dist n) . (p19,p29)))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10; Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7; then A34: H is open by TOPMETR:14, TOPMETR:20; A35: dist (p11,p22) <> 0 by A12, METRIC_1:2; then W in H by A32, A27, A28, TBSP_1:11, XREAL_1:139; then W in Int H by A34, TOPS_1:23; then reconsider H = H as a_neighborhood of W by CONNSP_2:def_1; take H ; ::_thesis: f .: H c= G A36: r / ((Pitag_dist n) . (p19,p29)) > 0 by A32, A27, A28, A35, XREAL_1:139; f .: H c= Ball (Y,r) proof reconsider WW1 = WW9 as Element of REAL n ; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in Ball (Y,r) ) A37: rng f c= the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) by RELAT_1:def_19; assume a in f .: H ; ::_thesis: a in Ball (Y,r) then consider u being set such that A38: u in dom f and A39: u in H and A40: a = f . u by FUNCT_1:def_6; reconsider u1 = u as Real by A3, A38; A41: [#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5; reconsider u9 = u as Point of (Closed-Interval-MSpace (0,1)) by A39; reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR:8; A42: dist (W9,u9) = the distance of (Closed-Interval-MSpace (0,1)) . (W9,u9) by METRIC_1:def_1 .= the distance of RealSpace . (W99,u99) by TOPMETR:def_1 .= dist (W99,u99) by METRIC_1:def_1 ; dist (W9,u9) < r / ((Pitag_dist n) . (p19,p29)) by A39, METRIC_1:11; then abs (W1 - u1) < r / ((Pitag_dist n) . (p19,p29)) by A42, TOPMETR:11; then abs (- (u1 - W1)) < r / ((Pitag_dist n) . (p19,p29)) ; then A43: abs (u1 - W1) < r / ((Pitag_dist n) . (p19,p29)) by COMPLEX1:52; A44: r / ((Pitag_dist n) . (p19,p29)) <> 0 by A32, A27, A28, A35, XREAL_1:139; then (Pitag_dist n) . (p19,p29) = r / (r / ((Pitag_dist n) . (p19,p29))) by XCMPLX_1:54; then A45: |.(p19 - p29).| = r / (r / ((Pitag_dist n) . (p19,p29))) by EUCLID:def_6; f . u in rng f by A38, FUNCT_1:def_3; then reconsider aa = a as Point of ((Euclid n) | PP) by A40, A37, A41, TOPMETR:def_2; LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2; then reconsider aa9 = aa as Point of (Euclid n) by TARSKI:def_3; reconsider aa1 = aa9 as Element of REAL n ; A46: p19 - p29 = p1 - p2 by EUCLID:69; A47: WW1 = ((1 - W1) * p1) + (W1 * p2) by A4, BORSUK_1:40; aa1 = ((1 - u1) * p1) + (u1 * p2) by A3, A4, A38, A40; then WW1 - aa1 = (((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2)) by A47, EUCLID:69 .= (((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2) by EUCLID:46 .= ((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2) by EUCLID:45 .= ((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2) by EUCLID:50 .= ((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2)) by EUCLID:45 .= ((u1 - W1) * p1) + ((W1 - u1) * p2) by EUCLID:50 .= ((u1 - W1) * p1) + ((- (u1 - W1)) * p2) .= ((u1 - W1) * p1) + (- ((u1 - W1) * p2)) by EUCLID:40 .= ((u1 - W1) * p1) - ((u1 - W1) * p2) by EUCLID:41 .= (u1 - W1) * (p1 - p2) by EUCLID:49 .= (u1 - W1) * (p19 - p29) by A46, EUCLID:65 ; then A48: |.(WW1 - aa1).| = (abs (u1 - W1)) * |.(p19 - p29).| by EUCLID:11; r / (r / ((Pitag_dist n) . (p19,p29))) > 0 by A32, A36, XREAL_1:139; then |.(WW1 - aa1).| < (r / ((Pitag_dist n) . (p19,p29))) * (r / (r / ((Pitag_dist n) . (p19,p29)))) by A48, A43, A45, XREAL_1:68; then |.(WW1 - aa1).| < r by A44, XCMPLX_1:87; then the distance of (Euclid n) . (WW9,aa9) < r by EUCLID:def_6; then the distance of ((Euclid n) | PP) . (Y,aa) < r by TOPMETR:def_1; then dist (Y,aa) < r by METRIC_1:def_1; hence a in Ball (Y,r) by METRIC_1:11; ::_thesis: verum end; then f .: H c= Q by A33, XBOOLE_1:1; hence f .: H c= G by A30, XBOOLE_1:1; ::_thesis: verum end; then A49: f is continuous by BORSUK_1:def_1; take f ; :: according to TOPREAL1:def_1 ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) A50: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider PP = LSeg (p1,p2) as Subset of (TopSpaceMetr (Euclid n)) ; (TopSpaceMetr (Euclid n)) | PP = (TOP-REAL n) | (LSeg (p1,p2)) by A50, PRE_TOPC:36; then (TOP-REAL n) | (LSeg (p1,p2)) is T_2 by A25, TOPMETR:2; hence f is being_homeomorphism by A3, A1, A24, A19, A49, A11, COMPTS_1:17; ::_thesis: ( f . 0 = p1 & f . 1 = p2 ) 0 in [.0,1.] by XXREAL_1:1; hence f . 0 = ((1 - 0) * p1) + (0 * p2) by A4 .= p1 + (0 * p2) by EUCLID:29 .= p1 + (0. (TOP-REAL n)) by EUCLID:29 .= p1 by EUCLID:27 ; ::_thesis: f . 1 = p2 1 in [.0,1.] by XXREAL_1:1; hence f . 1 = ((1 - 1) * p1) + (1 * p2) by A4 .= (0. (TOP-REAL n)) + (1 * p2) by EUCLID:29 .= 1 * p2 by EUCLID:27 .= p2 by EUCLID:29 ; ::_thesis: verum end; registration let n be Nat; cluster TOP-REAL n -> T_2 ; coherence TOP-REAL n is T_2 proof TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is T_2 by PCOMPS_1:34; hence TOP-REAL n is T_2 by Lm2; ::_thesis: verum end; end; theorem Th10: :: TOPREAL1:10 for n being Nat for P being Subset of (TOP-REAL n) for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 proof let n be Nat; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} implies P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 ) assume that A1: P is_an_arc_of p1,p2 and A2: P /\ (LSeg (p2,q1)) = {p2} ; ::_thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 percases ( p2 <> q1 or p2 = q1 ) ; suppose p2 <> q1 ; ::_thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 then LSeg (p2,q1) is_an_arc_of p2,q1 by Th9; hence P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A1, A2, Th2; ::_thesis: verum end; supposeA3: p2 = q1 ; ::_thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 then A4: LSeg (p2,q1) = {q1} by RLTOPSP1:70; q1 in P by A1, A3, Th1; hence P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A1, A3, A4, ZFMISC_1:40; ::_thesis: verum end; end; end; theorem Th11: :: TOPREAL1:11 for n being Nat for P being Subset of (TOP-REAL n) for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 proof let n be Nat; ::_thesis: for P being Subset of (TOP-REAL n) for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} implies (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 ) assume that A1: P is_an_arc_of p2,p1 and A2: (LSeg (q1,p2)) /\ P = {p2} ; ::_thesis: (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 percases ( p2 <> q1 or p2 = q1 ) ; suppose p2 <> q1 ; ::_thesis: (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 then LSeg (q1,p2) is_an_arc_of q1,p2 by Th9; hence (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 by A1, A2, Th2; ::_thesis: verum end; supposeA3: p2 = q1 ; ::_thesis: (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 then A4: LSeg (q1,p2) = {q1} by RLTOPSP1:70; q1 in P by A1, A3, Th1; hence (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 by A1, A3, A4, ZFMISC_1:40; ::_thesis: verum end; end; end; theorem :: TOPREAL1:12 for n being Nat for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 proof let n be Nat; ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} implies (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 ) assume that A1: ( p1 <> p2 or p2 <> q1 ) and A2: (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} ; ::_thesis: (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 percases ( p1 <> p2 or p2 <> q1 ) by A1; suppose p1 <> p2 ; ::_thesis: (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 hence (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A2, Th9, Th10; ::_thesis: verum end; suppose p2 <> q1 ; ::_thesis: (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 hence (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A2, Th9, Th11; ::_thesis: verum end; end; end; theorem Th13: :: TOPREAL1:13 ( LSeg (|[0,0]|,|[0,1]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } & LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } ) proof set p0 = |[0,0]|; set p01 = |[0,1]|; set p10 = |[1,0]|; set p1 = |[1,1]|; set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ; set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ; set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ; A1: |[0,1]| `2 = 1 by EUCLID:52; A2: |[0,1]| `1 = 0 by EUCLID:52; A3: LSeg (|[0,0]|,|[0,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[0,0]|,|[0,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ) assume a in LSeg (|[0,0]|,|[0,1]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } then consider lambda being Real such that A4: a = ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|) and A5: 0 <= lambda and A6: lambda <= 1 ; set q = ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|); A7: ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|) = (0. (TOP-REAL 2)) + (lambda * |[0,1]|) by EUCLID:28, EUCLID:54 .= lambda * |[0,1]| by EUCLID:27 .= |[(lambda * (|[0,1]| `1)),(lambda * (|[0,1]| `2))]| by EUCLID:57 .= |[0,lambda]| by A2, A1 ; then A8: (((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `2 >= 0 by A5, EUCLID:52; A9: (((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `1 = 0 by A7, EUCLID:52; (((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `2 <= 1 by A6, A7, EUCLID:52; hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A4, A9, A8; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } c= LSeg (|[0,0]|,|[0,1]|) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } or a in LSeg (|[0,0]|,|[0,1]|) ) assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ; ::_thesis: a in LSeg (|[0,0]|,|[0,1]|) then consider p being Point of (TOP-REAL 2) such that A10: a = p and A11: p `1 = 0 and A12: p `2 <= 1 and A13: p `2 >= 0 ; set lambda = p `2 ; ((1 - (p `2)) * |[0,0]|) + ((p `2) * |[0,1]|) = (0. (TOP-REAL 2)) + ((p `2) * |[0,1]|) by EUCLID:28, EUCLID:54 .= (p `2) * |[0,1]| by EUCLID:27 .= |[((p `2) * (|[0,1]| `1)),((p `2) * (|[0,1]| `2))]| by EUCLID:57 .= p by A2, A1, A11, EUCLID:53 ; hence a in LSeg (|[0,0]|,|[0,1]|) by A10, A12, A13; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } = LSeg (|[0,0]|,|[0,1]|) by A3, XBOOLE_0:def_10; ::_thesis: ( LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } ) A14: |[1,1]| `2 = 1 by EUCLID:52; A15: |[1,1]| `1 = 1 by EUCLID:52; A16: LSeg (|[0,1]|,|[1,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[0,1]|,|[1,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) assume a in LSeg (|[0,1]|,|[1,1]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } then consider lambda being Real such that A17: a = ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|) and A18: 0 <= lambda and A19: lambda <= 1 ; set q = ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|); A20: ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|) = |[((1 - lambda) * 0),((1 - lambda) * (|[0,1]| `2))]| + (lambda * |[1,1]|) by A2, EUCLID:57 .= |[0,(1 - lambda)]| + |[lambda,(lambda * 1)]| by A1, A15, A14, EUCLID:57 .= |[(0 + lambda),((1 - lambda) + lambda)]| by EUCLID:56 .= |[lambda,1]| ; then A21: (((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `1 >= 0 by A18, EUCLID:52; A22: (((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `2 = 1 by A20, EUCLID:52; (((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `1 <= 1 by A19, A20, EUCLID:52; hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } by A17, A21, A22; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } c= LSeg (|[0,1]|,|[1,1]|) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } or a in LSeg (|[0,1]|,|[1,1]|) ) assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ; ::_thesis: a in LSeg (|[0,1]|,|[1,1]|) then consider p being Point of (TOP-REAL 2) such that A23: a = p and A24: p `1 <= 1 and A25: p `1 >= 0 and A26: p `2 = 1 ; set lambda = p `1 ; ((1 - (p `1)) * |[0,1]|) + ((p `1) * |[1,1]|) = |[((1 - (p `1)) * 0),((1 - (p `1)) * (|[0,1]| `2))]| + ((p `1) * |[1,1]|) by A2, EUCLID:57 .= |[0,(1 - (p `1))]| + |[((p `1) * 1),(p `1)]| by A1, A15, A14, EUCLID:57 .= |[(0 + (p `1)),((1 - (p `1)) + (p `1))]| by EUCLID:56 .= p by A26, EUCLID:53 ; hence a in LSeg (|[0,1]|,|[1,1]|) by A23, A24, A25; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } = LSeg (|[0,1]|,|[1,1]|) by A16, XBOOLE_0:def_10; ::_thesis: ( LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } ) A27: |[1,0]| `2 = 0 by EUCLID:52; A28: |[1,0]| `1 = 1 by EUCLID:52; A29: LSeg (|[0,0]|,|[1,0]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[0,0]|,|[1,0]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) assume a in LSeg (|[0,0]|,|[1,0]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } then consider lambda being Real such that A30: a = ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|) and A31: 0 <= lambda and A32: lambda <= 1 ; set q = ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|); A33: ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|) = (0. (TOP-REAL 2)) + (lambda * |[1,0]|) by EUCLID:28, EUCLID:54 .= lambda * |[1,0]| by EUCLID:27 .= |[(lambda * (|[1,0]| `1)),(lambda * (|[1,0]| `2))]| by EUCLID:57 .= |[lambda,0]| by A28, A27 ; then A34: (((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `1 >= 0 by A31, EUCLID:52; A35: (((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `2 = 0 by A33, EUCLID:52; (((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `1 <= 1 by A32, A33, EUCLID:52; hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by A30, A34, A35; ::_thesis: verum end; A36: LSeg (|[1,0]|,|[1,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[1,0]|,|[1,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) assume a in LSeg (|[1,0]|,|[1,1]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } then consider lambda being Real such that A37: a = ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|) and A38: 0 <= lambda and A39: lambda <= 1 ; set q = ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|); A40: ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|) = |[((1 - lambda) * 1),((1 - lambda) * (|[1,0]| `2))]| + (lambda * |[1,1]|) by A28, EUCLID:57 .= |[(1 - lambda),0]| + |[lambda,(lambda * 1)]| by A15, A14, A27, EUCLID:57 .= |[((1 - lambda) + lambda),(0 + lambda)]| by EUCLID:56 .= |[1,lambda]| ; then A41: (((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `2 >= 0 by A38, EUCLID:52; A42: (((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `1 = 1 by A40, EUCLID:52; (((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `2 <= 1 by A39, A40, EUCLID:52; hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } by A37, A42, A41; ::_thesis: verum end; { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } c= LSeg (|[0,0]|,|[1,0]|) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } or a in LSeg (|[0,0]|,|[1,0]|) ) assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; ::_thesis: a in LSeg (|[0,0]|,|[1,0]|) then consider p being Point of (TOP-REAL 2) such that A43: a = p and A44: p `1 <= 1 and A45: p `1 >= 0 and A46: p `2 = 0 ; set lambda = p `1 ; ((1 - (p `1)) * |[0,0]|) + ((p `1) * |[1,0]|) = (0. (TOP-REAL 2)) + ((p `1) * |[1,0]|) by EUCLID:28, EUCLID:54 .= (p `1) * |[1,0]| by EUCLID:27 .= |[((p `1) * (|[1,0]| `1)),((p `1) * (|[1,0]| `2))]| by EUCLID:57 .= p by A28, A27, A46, EUCLID:53 ; hence a in LSeg (|[0,0]|,|[1,0]|) by A43, A44, A45; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = LSeg (|[0,0]|,|[1,0]|) by A29, XBOOLE_0:def_10; ::_thesis: LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } c= LSeg (|[1,0]|,|[1,1]|) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } or a in LSeg (|[1,0]|,|[1,1]|) ) assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ; ::_thesis: a in LSeg (|[1,0]|,|[1,1]|) then consider p being Point of (TOP-REAL 2) such that A47: a = p and A48: p `1 = 1 and A49: p `2 <= 1 and A50: p `2 >= 0 ; set lambda = p `2 ; ((1 - (p `2)) * |[1,0]|) + ((p `2) * |[1,1]|) = |[((1 - (p `2)) * 1),((1 - (p `2)) * (|[1,0]| `2))]| + ((p `2) * |[1,1]|) by A28, EUCLID:57 .= |[(1 - (p `2)),0]| + |[((p `2) * 1),(p `2)]| by A15, A14, A27, EUCLID:57 .= |[((1 - (p `2)) + (p `2)),(0 + (p `2))]| by EUCLID:56 .= p by A48, EUCLID:53 ; hence a in LSeg (|[1,0]|,|[1,1]|) by A47, A49, A50; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } = LSeg (|[1,0]|,|[1,1]|) by A36, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TOPREAL1:14 R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) } proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= 0 ); defpred S2[ Point of (TOP-REAL 2)] means ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 0 ); defpred S3[ Point of (TOP-REAL 2)] means ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 1 ); defpred S4[ Point of (TOP-REAL 2)] means ( $1 `1 = 0 & $1 `2 <= 1 & $1 `2 >= 0 ); defpred S5[ Point of (TOP-REAL 2)] means ( ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 0 ) or ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= 0 ) ); defpred S6[ Point of (TOP-REAL 2)] means ( ( $1 `1 = 0 & $1 `2 <= 1 & $1 `2 >= 0 ) or ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 1 ) ); set L1 = { p where p is Point of (TOP-REAL 2) : S4[p] } ; set L2 = { p where p is Point of (TOP-REAL 2) : S3[p] } ; set L3 = { p where p is Point of (TOP-REAL 2) : S2[p] } ; set L4 = { p where p is Point of (TOP-REAL 2) : S1[p] } ; A1: { p2 where p2 is Point of (TOP-REAL 2) : ( S6[p2] or S5[p2] ) } = { p where p is Point of (TOP-REAL 2) : S6[p] } \/ { q1 where q1 is Point of (TOP-REAL 2) : S5[q1] } from TOPREAL1:sch_1(); A2: { q1 where q1 is Point of (TOP-REAL 2) : ( S2[q1] or S1[q1] ) } = { p where p is Point of (TOP-REAL 2) : S2[p] } \/ { p where p is Point of (TOP-REAL 2) : S1[p] } from TOPREAL1:sch_1() .= (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) by Th13 ; { p where p is Point of (TOP-REAL 2) : ( S4[p] or S3[p] ) } = { p where p is Point of (TOP-REAL 2) : S4[p] } \/ { p where p is Point of (TOP-REAL 2) : S3[p] } from TOPREAL1:sch_1() .= (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) by Th13 ; hence R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) } by A1, A2; ::_thesis: verum end; registration cluster R^2-unit_square -> non empty ; coherence not R^2-unit_square is empty ; end; theorem :: TOPREAL1:15 (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,1]|} proof for a being set holds ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff a = |[0,1]| ) proof set p00 = |[0,0]|; set p01 = |[0,1]|; set p11 = |[1,1]|; let a be set ; ::_thesis: ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff a = |[0,1]| ) thus ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) implies a = |[0,1]| ) ::_thesis: ( a = |[0,1]| implies a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ) proof assume A1: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; ::_thesis: a = |[0,1]| then a in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } by Th13, XBOOLE_0:def_4; then A2: ex p2 being Point of (TOP-REAL 2) st ( p2 = a & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) ; a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A1, Th13, XBOOLE_0:def_4; then ex p being Point of (TOP-REAL 2) st ( p = a & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) ; hence a = |[0,1]| by A2, EUCLID:53; ::_thesis: verum end; assume A3: a = |[0,1]| ; ::_thesis: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) then A4: a in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68; a in LSeg (|[0,0]|,|[0,1]|) by A3, RLTOPSP1:68; hence a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,1]|} by TARSKI:def_1; ::_thesis: verum end; theorem :: TOPREAL1:16 (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|} proof for a being set holds ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,0]| ) proof set p00 = |[0,0]|; set p10 = |[1,0]|; set p11 = |[1,1]|; let a be set ; ::_thesis: ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,0]| ) thus ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies a = |[1,0]| ) ::_thesis: ( a = |[1,0]| implies a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ) proof assume A1: a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; ::_thesis: a = |[1,0]| then a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by Th13, XBOOLE_0:def_4; then A2: ex p being Point of (TOP-REAL 2) st ( p = a & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ; a in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def_4; then ex p2 being Point of (TOP-REAL 2) st ( p2 = a & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13; hence a = |[1,0]| by A2, EUCLID:53; ::_thesis: verum end; assume A3: a = |[1,0]| ; ::_thesis: a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) then A4: a in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68; a in LSeg (|[0,0]|,|[1,0]|) by A3, RLTOPSP1:68; hence a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|} by TARSKI:def_1; ::_thesis: verum end; theorem Th17: :: TOPREAL1:17 (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,0]|} proof for a being set holds ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) iff a = |[0,0]| ) proof let a be set ; ::_thesis: ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) iff a = |[0,0]| ) thus ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) implies a = |[0,0]| ) ::_thesis: ( a = |[0,0]| implies a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) ) proof assume A1: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; ::_thesis: a = |[0,0]| then a in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) } by Th13, XBOOLE_0:def_4; then A2: ex p2 being Point of (TOP-REAL 2) st ( p2 = a & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) ; a in LSeg (|[0,0]|,|[0,1]|) by A1, XBOOLE_0:def_4; then ex p being Point of (TOP-REAL 2) st ( p = a & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) by Th13; hence a = |[0,0]| by A2, EUCLID:53; ::_thesis: verum end; assume A3: a = |[0,0]| ; ::_thesis: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) then A4: a in LSeg (|[0,0]|,|[1,0]|) by RLTOPSP1:68; a in LSeg (|[0,0]|,|[0,1]|) by A3, RLTOPSP1:68; hence a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,0]|} by TARSKI:def_1; ::_thesis: verum end; theorem Th18: :: TOPREAL1:18 (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,1]|} proof for a being set holds ( a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,1]| ) proof let a be set ; ::_thesis: ( a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,1]| ) thus ( a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies a = |[1,1]| ) ::_thesis: ( a = |[1,1]| implies a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ) proof assume A1: a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; ::_thesis: a = |[1,1]| then a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } by Th13, XBOOLE_0:def_4; then A2: ex p being Point of (TOP-REAL 2) st ( p = a & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) ; a in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def_4; then ex p2 being Point of (TOP-REAL 2) st ( p2 = a & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13; hence a = |[1,1]| by A2, EUCLID:53; ::_thesis: verum end; assume A3: a = |[1,1]| ; ::_thesis: a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) then A4: a in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68; a in LSeg (|[0,1]|,|[1,1]|) by A3, RLTOPSP1:68; hence a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,1]|} by TARSKI:def_1; ::_thesis: verum end; theorem :: TOPREAL1:19 LSeg (|[0,0]|,|[1,0]|) misses LSeg (|[0,1]|,|[1,1]|) proof set x = the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)); assume A1: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) in LSeg (|[0,1]|,|[1,1]|) by XBOOLE_0:def_4; then A2: ex p being Point of (TOP-REAL 2) st ( p = the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) by Th13; the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) in LSeg (|[0,0]|,|[1,0]|) by A1, XBOOLE_0:def_4; then ex p2 being Point of (TOP-REAL 2) st ( p2 = the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) by Th13; hence contradiction by A2; ::_thesis: verum end; theorem Th20: :: TOPREAL1:20 LSeg (|[0,0]|,|[0,1]|) misses LSeg (|[1,0]|,|[1,1]|) proof set x = the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)); assume A1: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) in LSeg (|[0,0]|,|[0,1]|) by XBOOLE_0:def_4; then A2: ex p being Point of (TOP-REAL 2) st ( p = the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) by Th13; the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def_4; then ex p2 being Point of (TOP-REAL 2) st ( p2 = the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13; hence contradiction by A2; ::_thesis: verum end; definition let n be Nat; let f be FinSequence of (TOP-REAL n); let i be Nat; func LSeg (f,i) -> Subset of (TOP-REAL n) equals :Def3: :: TOPREAL1:def 3 LSeg ((f /. i),(f /. (i + 1))) if ( 1 <= i & i + 1 <= len f ) otherwise {} ; coherence ( ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) ) ) proof thus ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) ; ::_thesis: ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) ) assume ( i < 1 or len f < i + 1 ) ; ::_thesis: {} is Subset of (TOP-REAL n) {} (TOP-REAL n) is Subset of (TOP-REAL n) ; hence {} is Subset of (TOP-REAL n) ; ::_thesis: verum end; correctness consistency for b1 being Subset of (TOP-REAL n) holds verum; ; end; :: deftheorem Def3 defines LSeg TOPREAL1:def_3_:_ for n being Nat for f being FinSequence of (TOP-REAL n) for i being Nat holds ( ( 1 <= i & i + 1 <= len f implies LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies LSeg (f,i) = {} ) ); theorem Th21: :: TOPREAL1:21 for n, i being Nat for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) proof let n, i be Nat; ::_thesis: for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) let f be FinSequence of (TOP-REAL n); ::_thesis: ( 1 <= i & i + 1 <= len f implies ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) ) assume that A1: 1 <= i and A2: i + 1 <= len f ; ::_thesis: ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, Def3; hence ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) by RLTOPSP1:68; ::_thesis: verum end; definition let n be Nat; let f be FinSequence of (TOP-REAL n); func L~ f -> Subset of (TOP-REAL n) equals :: TOPREAL1:def 4 union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; coherence union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n) proof set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= bool the carrier of (TOP-REAL n) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or a in bool the carrier of (TOP-REAL n) ) assume a in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: a in bool the carrier of (TOP-REAL n) then ex i being Element of NAT st ( a = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ; hence a in bool the carrier of (TOP-REAL n) ; ::_thesis: verum end; then reconsider F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } as Subset-Family of (TOP-REAL n) ; union F is Subset of (TOP-REAL n) ; hence union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n) ; ::_thesis: verum end; end; :: deftheorem defines L~ TOPREAL1:def_4_:_ for n being Nat for f being FinSequence of (TOP-REAL n) holds L~ f = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; theorem Th22: :: TOPREAL1:22 for n being Nat for f being FinSequence of (TOP-REAL n) holds ( ( len f = 0 or len f = 1 ) iff L~ f = {} ) proof let n be Nat; ::_thesis: for f being FinSequence of (TOP-REAL n) holds ( ( len f = 0 or len f = 1 ) iff L~ f = {} ) let f be FinSequence of (TOP-REAL n); ::_thesis: ( ( len f = 0 or len f = 1 ) iff L~ f = {} ) thus ( ( len f = 0 or len f = 1 ) implies L~ f = {} ) ::_thesis: ( not L~ f = {} or len f = 0 or len f = 1 ) proof set L = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set x = the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; assume A1: ( len f = 0 or len f = 1 ) ; ::_thesis: L~ f = {} now__::_thesis:_L~_f_=_{} percases ( len f = 0 or len f = 0 + 1 ) by A1; supposeA2: len f = 0 ; ::_thesis: L~ f = {} now__::_thesis:_not__{__(LSeg_(f,i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_f_)__}__<>_{} assume { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } <> {} ; ::_thesis: contradiction then the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; then ex i being Element of NAT st ( the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ; hence contradiction by A2; ::_thesis: verum end; hence L~ f = {} by ZFMISC_1:2; ::_thesis: verum end; supposeA3: len f = 0 + 1 ; ::_thesis: L~ f = {} now__::_thesis:_not__{__(LSeg_(f,i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_f_)__}__<>_{} assume { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } <> {} ; ::_thesis: contradiction then the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; then ex i being Element of NAT st ( the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ; hence contradiction by A3, XREAL_1:6; ::_thesis: verum end; hence L~ f = {} by ZFMISC_1:2; ::_thesis: verum end; end; end; hence L~ f = {} ; ::_thesis: verum end; set L = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; assume A4: L~ f = {} ; ::_thesis: ( len f = 0 or len f = 1 ) assume that A5: len f <> 0 and A6: len f <> 1 ; ::_thesis: contradiction now__::_thesis:_not_len_f_<=_1 assume len f <= 1 ; ::_thesis: contradiction then len f < 0 + 1 by A6, XXREAL_0:1; hence contradiction by A5, NAT_1:13; ::_thesis: verum end; then A7: len f >= 1 + 1 by NAT_1:13; then LSeg (f,1) in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; then LSeg (f,1) = {} by A4, XBOOLE_1:3, ZFMISC_1:74; hence contradiction by A7, Th21; ::_thesis: verum end; theorem Th23: :: TOPREAL1:23 for n being Nat for f being FinSequence of (TOP-REAL n) st len f >= 2 holds L~ f <> {} proof let n be Nat; ::_thesis: for f being FinSequence of (TOP-REAL n) st len f >= 2 holds L~ f <> {} let f be FinSequence of (TOP-REAL n); ::_thesis: ( len f >= 2 implies L~ f <> {} ) assume A1: len f >= 2 ; ::_thesis: L~ f <> {} then not len f = 1 ; hence L~ f <> {} by A1, Th22; ::_thesis: verum end; definition let IT be FinSequence of (TOP-REAL 2); attrIT is special means :: TOPREAL1:def 5 for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds (IT /. i) `2 = (IT /. (i + 1)) `2 ; attrIT is unfolded means :Def6: :: TOPREAL1:def 6 for i being Nat st 1 <= i & i + 2 <= len IT holds (LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))}; attrIT is s.n.c. means :Def7: :: TOPREAL1:def 7 for i, j being Nat st i + 1 < j holds LSeg (IT,i) misses LSeg (IT,j); end; :: deftheorem defines special TOPREAL1:def_5_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is special iff for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds (IT /. i) `2 = (IT /. (i + 1)) `2 ); :: deftheorem Def6 defines unfolded TOPREAL1:def_6_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is unfolded iff for i being Nat st 1 <= i & i + 2 <= len IT holds (LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))} ); :: deftheorem Def7 defines s.n.c. TOPREAL1:def_7_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is s.n.c. iff for i, j being Nat st i + 1 < j holds LSeg (IT,i) misses LSeg (IT,j) ); definition let f be FinSequence of (TOP-REAL 2); attrf is being_S-Seq means :Def8: :: TOPREAL1:def 8 ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ); end; :: deftheorem Def8 defines being_S-Seq TOPREAL1:def_8_:_ for f being FinSequence of (TOP-REAL 2) holds ( f is being_S-Seq iff ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) ); theorem Th24: :: TOPREAL1:24 ex f1, f2 being FinSequence of (TOP-REAL 2) st ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) proof set p0 = |[0,0]|; set p01 = |[0,1]|; set p10 = |[1,0]|; set p1 = |[1,1]|; set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ; set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ; set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ; A1: |[1,1]| `1 = 1 by EUCLID:52; reconsider f2 = <*|[0,0]|,|[1,0]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ; reconsider f1 = <*|[0,0]|,|[0,1]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ; A2: |[0,0]| `1 = 0 by EUCLID:52; take f1 ; ::_thesis: ex f2 being FinSequence of (TOP-REAL 2) st ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) take f2 ; ::_thesis: ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) A3: f1 /. 2 = |[0,1]| by FINSEQ_4:18; now__::_thesis:_not__{__p_where_p_is_Point_of_(TOP-REAL_2)_:_(_p_`1_<=_1_&_p_`1_>=_0_&_p_`2_=_1_)__}__meets__{__p_where_p_is_Point_of_(TOP-REAL_2)_:_(_p_`1_<=_1_&_p_`1_>=_0_&_p_`2_=_0_)__}_ assume { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; ::_thesis: contradiction then consider x being set such that A4: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } and A5: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by XBOOLE_0:3; A6: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) by A5; ex p being Point of (TOP-REAL 2) st ( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) by A4; hence contradiction by A6; ::_thesis: verum end; then A7: { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = {} by XBOOLE_0:def_7; A8: |[1,0]| `2 = 0 by EUCLID:52; A9: |[1,0]| `1 = 1 by EUCLID:52; A10: len f2 = 1 + 2 by FINSEQ_1:45; then A11: 1 + 1 <= len f2 ; A12: f1 /. 3 = |[1,1]| by FINSEQ_4:18; A13: f1 /. 1 = |[0,0]| by FINSEQ_4:18; A14: { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } or a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} ) assume a in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ; ::_thesis: a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} then consider i being Element of NAT such that A15: a = LSeg (f1,i) and A16: 1 <= i and A17: i + 1 <= len f1 ; i + 1 <= 2 + 1 by A17, FINSEQ_1:45; then i <= 1 + 1 by XREAL_1:6; then ( i = 1 or i = 2 ) by A16, NAT_1:9; then ( a = LSeg (|[0,0]|,|[0,1]|) or a = LSeg (|[0,1]|,|[1,1]|) ) by A13, A3, A12, A15, A17, Def3; hence a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} by TARSKI:def_2; ::_thesis: verum end; A18: len f1 = 1 + 2 by FINSEQ_1:45; then A19: 1 + 1 <= len f1 ; 1 + 1 in Seg (len f1) by A18, FINSEQ_1:1; then LSeg (|[0,0]|,|[0,1]|) = LSeg (f1,1) by A18, A13, A3, Def3; then A20: LSeg (|[0,0]|,|[0,1]|) in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A19; A21: f2 /. 3 = |[1,1]| by FINSEQ_4:18; A22: |[0,0]| `2 = 0 by EUCLID:52; thus f1 is being_S-Seq ::_thesis: ( f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) proof A23: |[0,1]| <> |[1,1]| by A1, EUCLID:52; |[0,0]| <> |[0,1]| by A22, EUCLID:52; hence f1 is one-to-one by A1, A2, A23, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( len f1 >= 2 & f1 is unfolded & f1 is s.n.c. & f1 is special ) thus len f1 >= 2 by A18; ::_thesis: ( f1 is unfolded & f1 is s.n.c. & f1 is special ) thus f1 is unfolded ::_thesis: ( f1 is s.n.c. & f1 is special ) proof A24: for x being set holds ( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff x = |[0,1]| ) proof let x be set ; ::_thesis: ( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff x = |[0,1]| ) thus ( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) implies x = |[0,1]| ) ::_thesis: ( x = |[0,1]| implies x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ) proof assume A25: x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; ::_thesis: x = |[0,1]| then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } by Th13, XBOOLE_0:def_4; then A26: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) ; x in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A25, Th13, XBOOLE_0:def_4; then ex p being Point of (TOP-REAL 2) st ( p = x & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) ; hence x = |[0,1]| by A26, EUCLID:53; ::_thesis: verum end; assume A27: x = |[0,1]| ; ::_thesis: x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) then A28: x in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68; x in LSeg (|[0,0]|,|[0,1]|) by A27, RLTOPSP1:68; hence x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A28, XBOOLE_0:def_4; ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( 1 <= i & i + 2 <= len f1 implies (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} ) assume that A29: 1 <= i and A30: i + 2 <= len f1 ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} i <= 1 by A18, A30, XREAL_1:6; then A31: i = 1 by A29, XXREAL_0:1; 1 + 1 in Seg (len f1) by A18, FINSEQ_1:1; then A32: LSeg (f1,1) = LSeg (|[0,0]|,|[0,1]|) by A18, A13, A3, Def3; LSeg (f1,(1 + 1)) = LSeg (|[0,1]|,|[1,1]|) by A18, A3, A12, Def3; hence (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} by A3, A31, A32, A24, TARSKI:def_1; ::_thesis: verum end; thus f1 is s.n.c. ::_thesis: f1 is special proof let i be Nat; :: according to TOPREAL1:def_7 ::_thesis: for j being Nat st i + 1 < j holds LSeg (f1,i) misses LSeg (f1,j) let j be Nat; ::_thesis: ( i + 1 < j implies LSeg (f1,i) misses LSeg (f1,j) ) assume A33: i + 1 < j ; ::_thesis: LSeg (f1,i) misses LSeg (f1,j) now__::_thesis:_(LSeg_(f1,i))_/\_(LSeg_(f1,j))_=_{} percases ( 1 <= i or not 1 <= i or not i + 1 <= len f1 ) ; suppose 1 <= i ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} then A34: 1 + 1 <= i + 1 by XREAL_1:6; now__::_thesis:_(_(_1_<=_j_&_j_+_1_<=_len_f1_&_contradiction_)_or_(_(_not_1_<=_j_or_not_j_+_1_<=_len_f1_)_&_(LSeg_(f1,i))_/\_(LSeg_(f1,j))_=_{}_)_) percases ( ( 1 <= j & j + 1 <= len f1 ) or not 1 <= j or not j + 1 <= len f1 ) ; case ( 1 <= j & j + 1 <= len f1 ) ; ::_thesis: contradiction then j <= 2 by A18, XREAL_1:6; hence contradiction by A33, A34, XXREAL_0:2; ::_thesis: verum end; case ( not 1 <= j or not j + 1 <= len f1 ) ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} then LSeg (f1,j) = {} by Def3; hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; ::_thesis: verum end; suppose ( not 1 <= i or not i + 1 <= len f1 ) ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} then LSeg (f1,i) = {} by Def3; hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( 1 <= i & i + 1 <= len f1 & not (f1 /. i) `1 = (f1 /. (i + 1)) `1 implies (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) assume that A35: 1 <= i and A36: i + 1 <= len f1 ; ::_thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) A37: i <= 1 + 1 by A18, A36, XREAL_1:6; percases ( i = 1 or i = 2 ) by A35, A37, NAT_1:9; supposeA38: i = 1 ; ::_thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) then (f1 /. i) `1 = |[0,0]| `1 by FINSEQ_4:18 .= 0 by EUCLID:52 .= (f1 /. (i + 1)) `1 by A3, A38, EUCLID:52 ; hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; ::_thesis: verum end; supposeA39: i = 2 ; ::_thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) then (f1 /. i) `2 = |[0,1]| `2 by FINSEQ_4:18 .= 1 by EUCLID:52 .= (f1 /. (i + 1)) `2 by A12, A39, EUCLID:52 ; hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; ::_thesis: verum end; end; end; A40: f2 /. 2 = |[1,0]| by FINSEQ_4:18; A41: f2 /. 1 = |[0,0]| by FINSEQ_4:18; A42: { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } or a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} ) assume a in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ; ::_thesis: a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} then consider i being Element of NAT such that A43: a = LSeg (f2,i) and A44: 1 <= i and A45: i + 1 <= len f2 ; i + 1 <= 2 + 1 by A45, FINSEQ_1:45; then i <= 1 + 1 by XREAL_1:6; then ( i = 1 or i = 2 ) by A44, NAT_1:9; then ( a = LSeg (|[0,0]|,|[1,0]|) or a = LSeg (|[1,0]|,|[1,1]|) ) by A41, A40, A21, A43, A45, Def3; hence a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} by TARSKI:def_2; ::_thesis: verum end; 1 + 1 in Seg (len f2) by A10, FINSEQ_1:1; then LSeg (|[0,0]|,|[1,0]|) = LSeg (f2,1) by A10, A41, A40, Def3; then A46: LSeg (|[0,0]|,|[1,0]|) in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A11; LSeg (|[1,0]|,|[1,1]|) = LSeg (f2,2) by A10, A40, A21, Def3; then LSeg (|[1,0]|,|[1,1]|) in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A10; then {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} c= { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A46, ZFMISC_1:32; then A47: L~ f2 = union {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} by A42, XBOOLE_0:def_10; A48: |[1,1]| `2 = 1 by EUCLID:52; thus f2 is being_S-Seq ::_thesis: ( R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) proof thus f2 is one-to-one by A1, A48, A9, A8, A2, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( len f2 >= 2 & f2 is unfolded & f2 is s.n.c. & f2 is special ) thus len f2 >= 2 by A10; ::_thesis: ( f2 is unfolded & f2 is s.n.c. & f2 is special ) thus f2 is unfolded ::_thesis: ( f2 is s.n.c. & f2 is special ) proof A49: for x being set holds ( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff x = |[1,0]| ) proof let x be set ; ::_thesis: ( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff x = |[1,0]| ) thus ( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies x = |[1,0]| ) ::_thesis: ( x = |[1,0]| implies x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ) proof assume A50: x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; ::_thesis: x = |[1,0]| then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) } by Th13, XBOOLE_0:def_4; then A51: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) ; x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by A50, Th13, XBOOLE_0:def_4; then ex p being Point of (TOP-REAL 2) st ( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ; hence x = |[1,0]| by A51, EUCLID:53; ::_thesis: verum end; assume A52: x = |[1,0]| ; ::_thesis: x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) then A53: x in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68; x in LSeg (|[0,0]|,|[1,0]|) by A52, RLTOPSP1:68; hence x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A53, XBOOLE_0:def_4; ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( 1 <= i & i + 2 <= len f2 implies (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))} ) assume that A54: 1 <= i and A55: i + 2 <= len f2 ; ::_thesis: (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))} i <= 1 by A10, A55, XREAL_1:6; then A56: i = 1 by A54, XXREAL_0:1; 1 + 1 in Seg (len f2) by A10, FINSEQ_1:1; then A57: LSeg (f2,1) = LSeg (|[0,0]|,|[1,0]|) by A10, A41, A40, Def3; LSeg (f2,(1 + 1)) = LSeg (|[1,0]|,|[1,1]|) by A10, A40, A21, Def3; hence (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))} by A40, A56, A57, A49, TARSKI:def_1; ::_thesis: verum end; thus f2 is s.n.c. ::_thesis: f2 is special proof let i be Nat; :: according to TOPREAL1:def_7 ::_thesis: for j being Nat st i + 1 < j holds LSeg (f2,i) misses LSeg (f2,j) let j be Nat; ::_thesis: ( i + 1 < j implies LSeg (f2,i) misses LSeg (f2,j) ) assume A58: i + 1 < j ; ::_thesis: LSeg (f2,i) misses LSeg (f2,j) percases ( 1 <= i or not 1 <= i or not i + 1 <= len f2 ) ; suppose 1 <= i ; ::_thesis: LSeg (f2,i) misses LSeg (f2,j) then A59: 1 + 1 <= i + 1 by XREAL_1:6; now__::_thesis:_(_(_1_<=_j_&_j_+_1_<=_len_f2_&_contradiction_)_or_(_(_not_1_<=_j_or_not_j_+_1_<=_len_f2_)_&_(LSeg_(f2,i))_/\_(LSeg_(f2,j))_=_{}_)_) percases ( ( 1 <= j & j + 1 <= len f2 ) or not 1 <= j or not j + 1 <= len f2 ) ; case ( 1 <= j & j + 1 <= len f2 ) ; ::_thesis: contradiction then j <= 2 by A10, XREAL_1:6; hence contradiction by A58, A59, XXREAL_0:2; ::_thesis: verum end; case ( not 1 <= j or not j + 1 <= len f2 ) ; ::_thesis: (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} then LSeg (f2,j) = {} by Def3; hence (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ; ::_thesis: verum end; end; end; hence (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; suppose ( not 1 <= i or not i + 1 <= len f2 ) ; ::_thesis: LSeg (f2,i) misses LSeg (f2,j) then LSeg (f2,i) = {} by Def3; hence (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; end; end; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( 1 <= i & i + 1 <= len f2 & not (f2 /. i) `1 = (f2 /. (i + 1)) `1 implies (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) assume that A60: 1 <= i and A61: i + 1 <= len f2 ; ::_thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) A62: i <= 1 + 1 by A10, A61, XREAL_1:6; percases ( i = 1 or i = 2 ) by A60, A62, NAT_1:9; supposeA63: i = 1 ; ::_thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) then (f2 /. i) `2 = |[0,0]| `2 by FINSEQ_4:18 .= 0 by EUCLID:52 .= (f2 /. (i + 1)) `2 by A40, A63, EUCLID:52 ; hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; ::_thesis: verum end; supposeA64: i = 2 ; ::_thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) then (f2 /. i) `1 = |[1,0]| `1 by FINSEQ_4:18 .= 1 by EUCLID:52 .= (f2 /. (i + 1)) `1 by A21, A64, EUCLID:52 ; hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; ::_thesis: verum end; end; end; A65: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by Th20, XBOOLE_0:def_7; LSeg (|[0,1]|,|[1,1]|) = LSeg (f1,2) by A18, A3, A12, Def3; then LSeg (|[0,1]|,|[1,1]|) in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A18; then {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} c= { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A20, ZFMISC_1:32; then A66: L~ f1 = union {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} by A14, XBOOLE_0:def_10; then L~ f1 = (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:75; hence R^2-unit_square = (L~ f1) \/ (L~ f2) by A47, ZFMISC_1:75; ::_thesis: ( (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) L~ f2 = (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) by A47, ZFMISC_1:75; hence (L~ f1) /\ (L~ f2) = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by A66, Th13, ZFMISC_1:75 .= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by XBOOLE_1:23 .= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by XBOOLE_1:23 .= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } )) by XBOOLE_1:23 .= {|[0,0]|,|[1,1]|} by A7, A65, Th13, Th17, Th18, ENUMSET1:1 ; ::_thesis: ( f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) thus ( f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) by A18, A10, FINSEQ_4:18; ::_thesis: verum end; theorem Th25: :: TOPREAL1:25 for h being FinSequence of (TOP-REAL 2) st h is being_S-Seq holds L~ h is_an_arc_of h /. 1,h /. (len h) proof let h be FinSequence of (TOP-REAL 2); ::_thesis: ( h is being_S-Seq implies L~ h is_an_arc_of h /. 1,h /. (len h) ) set P = L~ h; set p1 = h /. 1; deffunc H1( Nat) -> Subset of (TOP-REAL 2) = L~ (h | ($1 + 2)); defpred S1[ Nat] means ( 1 <= $1 + 2 & $1 + 2 <= len h implies ex NE being non empty Subset of (TOP-REAL 2) st ( NE = H1($1) & ex f being Function of I[01],((TOP-REAL 2) | NE) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ($1 + 2) ) ) ); set p2 = h /. (1 + 1); assume A1: h is being_S-Seq ; ::_thesis: L~ h is_an_arc_of h /. 1,h /. (len h) then A2: len h >= 1 + 1 by Def8; then 1 <= len h by XXREAL_0:2; then A3: 1 in Seg (len h) by FINSEQ_1:1; A4: h is one-to-one by A1, Def8; A5: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A6: S1[n] ; ::_thesis: S1[n + 1] set pn = h /. (n + 2); set pn1 = h /. ((n + 2) + 1); A7: (n + 1) + 1 <> (n + 2) + 1 ; reconsider NE1 = H1(n) \/ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) as non empty Subset of (TOP-REAL 2) ; assume that A8: 1 <= (n + 1) + 2 and A9: (n + 1) + 2 <= len h ; ::_thesis: ex NE being non empty Subset of (TOP-REAL 2) st ( NE = H1(n + 1) & ex f being Function of I[01],((TOP-REAL 2) | NE) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) ) A10: (n + 2) + 1 in dom h by A8, A9, FINSEQ_3:25; A11: (n + 1) + 1 <= (n + 2) + 1 by NAT_1:11; then consider NE being non empty Subset of (TOP-REAL 2) such that A12: NE = H1(n) and A13: ex f being Function of I[01],((TOP-REAL 2) | NE) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (n + 2) ) by A6, A9, NAT_1:11, XXREAL_0:2; A14: (n + 1) + 1 = n + (1 + 1) ; now__::_thesis:_for_x_being_set_st_x_in_H1(n)_\/_(LSeg_(h,(n_+_2)))_holds_ x_in_H1(n_+_1) let x be set ; ::_thesis: ( x in H1(n) \/ (LSeg (h,(n + 2))) implies x in H1(n + 1) ) assume A15: x in H1(n) \/ (LSeg (h,(n + 2))) ; ::_thesis: x in H1(n + 1) now__::_thesis:_x_in_H1(n_+_1) percases ( x in H1(n) or x in LSeg (h,(n + 2)) ) by A15, XBOOLE_0:def_3; supposeA16: x in H1(n) ; ::_thesis: x in H1(n + 1) A17: n + 1 <= n + (1 + 1) by XREAL_1:6; consider X being set such that A18: x in X and A19: X in { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A16, TARSKI:def_4; consider i being Element of NAT such that A20: X = LSeg ((h | (n + 2)),i) and A21: 1 <= i and A22: i + 1 <= len (h | (n + 2)) by A19; i + 1 <= (n + 1) + 1 by A9, A11, A22, FINSEQ_1:59, XXREAL_0:2; then i <= n + 1 by XREAL_1:6; then A23: i <= n + 2 by A17, XXREAL_0:2; len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:59, XXREAL_0:2; then i in Seg (len (h | (n + 2))) by A21, A23, FINSEQ_1:1; then A24: i in dom (h | (n + 2)) by FINSEQ_1:def_3; set p19 = (h | (n + 2)) /. i; set p29 = (h | (n + 2)) /. (i + 1); A25: n + 2 <= (n + 2) + 1 by NAT_1:11; then i <= (n + 1) + 2 by A23, XXREAL_0:2; then i in Seg ((n + 1) + 2) by A21, FINSEQ_1:1; then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59; then i in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A26: (h | ((n + 1) + 2)) /. i = h /. i by FINSEQ_4:70 .= (h | (n + 2)) /. i by A24, FINSEQ_4:70 ; i + 1 <= n + 2 by A9, A11, A22, FINSEQ_1:59, XXREAL_0:2; then A27: i + 1 <= (n + 1) + 2 by A25, XXREAL_0:2; A28: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59; A29: len (h | ((n + 1) + 2)) = n + (1 + 2) by A9, FINSEQ_1:59; A30: n + 2 <= n + 3 by XREAL_1:6; 1 <= i + 1 by NAT_1:11; then i + 1 in Seg (len (h | (n + 2))) by A22, FINSEQ_1:1; then A31: i + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3; 1 <= 1 + i by NAT_1:11; then i + 1 in Seg ((n + 1) + 2) by A27, FINSEQ_1:1; then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59; then i + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A32: (h | ((n + 1) + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:70 .= (h | (n + 2)) /. (i + 1) by A31, FINSEQ_4:70 ; i + 1 <= n + (1 + 1) by A9, A11, A22, FINSEQ_1:59, XXREAL_0:2; then A33: i + 1 <= len (h | ((n + 1) + 2)) by A29, A30, XXREAL_0:2; X = LSeg (((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1))) by A20, A21, A22, Def3 .= LSeg ((h | ((n + 1) + 2)),i) by A21, A27, A28, A26, A32, Def3 ; then X in { (LSeg ((h | ((n + 1) + 2)),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | ((n + 1) + 2)) ) } by A21, A33; hence x in H1(n + 1) by A18, TARSKI:def_4; ::_thesis: verum end; supposeA34: x in LSeg (h,(n + 2)) ; ::_thesis: x in H1(n + 1) A35: 1 <= n + 2 by A14, NAT_1:11; A36: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59; then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A8, FINSEQ_1:1; then A37: (n + 2) + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A38: (n + 2) + 1 <= len (h | ((n + 1) + 2)) by FINSEQ_3:25; n + 2 <= (n + 2) + 1 by NAT_1:11; then n + 2 in Seg (len (h | ((n + 1) + 2))) by A36, A35, FINSEQ_1:1; then A39: n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A40: 1 <= n + 2 by FINSEQ_3:25; A41: h /. ((n + 2) + 1) = (h | ((n + 1) + 2)) /. ((n + 2) + 1) by A37, FINSEQ_4:70; A42: h /. (n + 2) = (h | ((n + 1) + 2)) /. (n + 2) by A39, FINSEQ_4:70; LSeg (h,(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A9, A35, Def3 .= LSeg ((h | ((n + 1) + 2)),(n + 2)) by A36, A35, A42, A41, Def3 ; then LSeg (h,(n + 2)) in { (LSeg ((h | ((n + 1) + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by A40, A38; hence x in H1(n + 1) by A34, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in H1(n + 1) ; ::_thesis: verum end; then A43: H1(n) \/ (LSeg (h,(n + 2))) c= H1(n + 1) by TARSKI:def_3; take NE1 ; ::_thesis: ( NE1 = H1(n + 1) & ex f being Function of I[01],((TOP-REAL 2) | NE1) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) ) A44: 1 <= (n + 1) + 1 by NAT_1:11; now__::_thesis:_for_x_being_set_st_x_in_H1(n_+_1)_holds_ x_in_H1(n)_\/_(LSeg_(h,(n_+_2))) let x be set ; ::_thesis: ( x in H1(n + 1) implies x in H1(n) \/ (LSeg (h,(n + 2))) ) A45: n + (1 + 1) = (n + 1) + 1 ; A46: (len (h | ((n + 1) + 2))) - 1 = ((n + 1) + 2) - 1 by A9, FINSEQ_1:59 .= n + (1 + 1) ; assume x in H1(n + 1) ; ::_thesis: x in H1(n) \/ (LSeg (h,(n + 2))) then consider X being set such that A47: x in X and A48: X in { (LSeg ((h | ((n + 1) + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by TARSKI:def_4; consider i being Element of NAT such that A49: X = LSeg ((h | ((n + 1) + 2)),i) and A50: 1 <= i and A51: i + 1 <= len (h | ((n + 1) + 2)) by A48; (i + 1) - 1 = i ; then A52: i <= (len (h | ((n + 1) + 2))) - 1 by A51, XREAL_1:9; now__::_thesis:_x_in_H1(n)_\/_(LSeg_(h,(n_+_2))) percases ( i = n + 2 or i <= n + 1 ) by A52, A46, A45, NAT_1:8; supposeA53: i = n + 2 ; ::_thesis: x in H1(n) \/ (LSeg (h,(n + 2))) A54: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59; 1 <= (n + 2) + 1 by NAT_1:11; then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A54, FINSEQ_1:1; then (n + 2) + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A55: (h | ((n + 1) + 2)) /. ((n + 2) + 1) = h /. (n + (2 + 1)) by FINSEQ_4:70; A56: 1 <= n + 2 by A14, NAT_1:11; (n + 1) + 2 = (n + 2) + 1 ; then n + 2 <= (n + 1) + 2 by NAT_1:11; then n + 2 in Seg (len (h | ((n + 1) + 2))) by A54, A56, FINSEQ_1:1; then n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then (h | ((n + 1) + 2)) /. (n + 2) = h /. (n + 2) by FINSEQ_4:70; then LSeg ((h | ((n + 1) + 2)),(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A54, A56, A55, Def3 .= LSeg (h,(n + 2)) by A9, A44, Def3 ; hence x in H1(n) \/ (LSeg (h,(n + 2))) by A47, A49, A53, XBOOLE_0:def_3; ::_thesis: verum end; supposeA57: i <= n + 1 ; ::_thesis: x in H1(n) \/ (LSeg (h,(n + 2))) then i + 1 <= (n + 1) + 1 by XREAL_1:6; then i + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:59, XXREAL_0:2; then A58: LSeg ((h | (n + 2)),i) in { (LSeg ((h | (n + 2)),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A50; set p19 = (h | (n + 2)) /. i; set p29 = (h | (n + 2)) /. (i + 1); A59: 1 <= 1 + i by NAT_1:11; A60: len (h | (n + 2)) = n + (1 + 1) by A9, A11, FINSEQ_1:59, XXREAL_0:2; n + 1 <= (n + 1) + 1 by NAT_1:11; then A61: i <= n + 2 by A57, XXREAL_0:2; then i in Seg (len (h | (n + 2))) by A50, A60, FINSEQ_1:1; then A62: i in dom (h | (n + 2)) by FINSEQ_1:def_3; A63: i + 1 <= (n + 1) + 1 by A57, XREAL_1:7; then i + 1 in Seg (len (h | (n + 2))) by A60, A59, FINSEQ_1:1; then A64: i + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3; n + 2 <= (n + 2) + 1 by NAT_1:11; then i <= (n + 1) + 2 by A61, XXREAL_0:2; then i in Seg ((n + 1) + 2) by A50, FINSEQ_1:1; then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59; then i in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A65: (h | ((n + 1) + 2)) /. i = h /. i by FINSEQ_4:70 .= (h | (n + 2)) /. i by A62, FINSEQ_4:70 ; i + 1 <= (n + 1) + 2 by A57, XREAL_1:7; then i + 1 in Seg ((n + 1) + 2) by A59, FINSEQ_1:1; then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59; then i + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3; then A66: (h | ((n + 1) + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:70 .= (h | (n + 2)) /. (i + 1) by A64, FINSEQ_4:70 ; LSeg ((h | (n + 2)),i) = LSeg (((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1))) by A50, A60, A63, Def3 .= LSeg ((h | ((n + 1) + 2)),i) by A50, A51, A65, A66, Def3 ; then x in union { (LSeg ((h | (n + 2)),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A47, A49, A58, TARSKI:def_4; hence x in H1(n) \/ (LSeg (h,(n + 2))) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence x in H1(n) \/ (LSeg (h,(n + 2))) ; ::_thesis: verum end; then H1(n + 1) c= H1(n) \/ (LSeg (h,(n + 2))) by TARSKI:def_3; then H1(n + 1) = H1(n) \/ (LSeg (h,(n + 2))) by A43, XBOOLE_0:def_10; hence NE1 = H1(n + 1) by A9, A44, Def3; ::_thesis: ex f being Function of I[01],((TOP-REAL 2) | NE1) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) A67: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2; then (n + 1) + 1 in dom h by A44, FINSEQ_3:25; then LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) is_an_arc_of h /. (n + 2),h /. ((n + 2) + 1) by A4, A7, A10, Th9, PARTFUN2:10; then consider f1 being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))))) such that A68: f1 is being_homeomorphism and A69: f1 . 0 = h /. (n + 2) and A70: f1 . 1 = h /. ((n + 2) + 1) by Def1; consider f being Function of I[01],((TOP-REAL 2) | NE) such that f is being_homeomorphism and A71: f . 0 = h /. 1 and f . 1 = h /. (n + 2) by A13; for x being set holds ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) iff x = h /. (n + 2) ) proof let x be set ; ::_thesis: ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) iff x = h /. (n + 2) ) A72: 1 <= n + 1 by NAT_1:11; thus ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) implies x = h /. (n + 2) ) ::_thesis: ( x = h /. (n + 2) implies x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) ) proof A73: 1 <= n + 1 by NAT_1:11; h is unfolded by A1, Def8; then A74: (LSeg (h,(n + 1))) /\ (LSeg (h,((n + 1) + 1))) = {(h /. ((n + 1) + 1))} by A9, A73, Def6; A75: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2; assume A76: x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) ; ::_thesis: x = h /. (n + 2) then A77: x in LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by XBOOLE_0:def_4; A78: LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) = LSeg (h,((n + 1) + 1)) by A9, A44, Def3; set p19 = h /. (n + 1); set p29 = h /. ((n + 1) + 1); A79: 1 <= 1 + n by NAT_1:11; x in H1(n) by A76, XBOOLE_0:def_4; then consider X being set such that A80: x in X and A81: X in { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by TARSKI:def_4; consider i being Element of NAT such that A82: X = LSeg ((h | (n + 2)),i) and A83: 1 <= i and A84: i + 1 <= len (h | (n + 2)) by A81; A85: len (h | (n + 2)) = n + (1 + 1) by A9, A11, FINSEQ_1:59, XXREAL_0:2; n + 1 <= (n + 1) + 1 by NAT_1:11; then n + 1 in Seg (len (h | (n + 2))) by A85, A79, FINSEQ_1:1; then n + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3; then A86: (h | (n + 2)) /. (n + 1) = h /. (n + 1) by FINSEQ_4:70; 1 <= 1 + (n + 1) by NAT_1:11; then (n + 1) + 1 in Seg (len (h | (n + 2))) by A85, FINSEQ_1:1; then (n + 1) + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3; then A87: (h | (n + 2)) /. ((n + 1) + 1) = h /. ((n + 1) + 1) by FINSEQ_4:70; A88: len (h | (n + 2)) = (n + 1) + 1 by A9, A11, FINSEQ_1:59, XXREAL_0:2; then A89: i <= n + 1 by A84, XREAL_1:6; then 1 <= n + 1 by A83, XXREAL_0:2; then A90: LSeg (h,(n + 1)) = LSeg ((h /. (n + 1)),(h /. ((n + 1) + 1))) by A75, Def3 .= LSeg ((h | (n + 2)),(n + 1)) by A85, A79, A86, A87, Def3 ; A91: h is s.n.c. by A1, Def8; now__::_thesis:_not_i_<_n_+_1 set p19 = h /. i; set p29 = h /. (i + 1); assume A92: i < n + 1 ; ::_thesis: contradiction then A93: i + 1 < (n + 1) + 1 by XREAL_1:6; n + 1 <= (n + 1) + 1 by NAT_1:11; then i <= n + 2 by A92, XXREAL_0:2; then i in Seg (len (h | (n + 2))) by A83, A85, FINSEQ_1:1; then i in dom (h | (n + 2)) by FINSEQ_1:def_3; then A94: (h | (n + 2)) /. i = h /. i by FINSEQ_4:70; A95: LSeg (h,(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A9, A44, Def3; 1 <= 1 + i by NAT_1:11; then i + 1 in Seg (len (h | (n + 2))) by A84, FINSEQ_1:1; then i + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3; then A96: (h | (n + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:70; i + 1 <= len h by A67, A84, A88, XXREAL_0:2; then LSeg (h,i) = LSeg ((h /. i),(h /. (i + 1))) by A83, Def3 .= LSeg ((h | (n + 2)),i) by A83, A84, A94, A96, Def3 ; then LSeg ((h | (n + 2)),i) misses LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A91, A93, A95, Def7; hence contradiction by A77, A80, A82, XBOOLE_0:3; ::_thesis: verum end; then i = n + 1 by A89, XXREAL_0:1; then x in (LSeg (h,(n + 1))) /\ (LSeg (h,((n + 1) + 1))) by A77, A80, A82, A90, A78, XBOOLE_0:def_4; hence x = h /. (n + 2) by A74, TARSKI:def_1; ::_thesis: verum end; assume A97: x = h /. (n + 2) ; ::_thesis: x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) A98: 1 <= n + 1 by NAT_1:11; (n + 1) + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:59, XXREAL_0:2; then A99: LSeg ((h | (n + 2)),(n + 1)) in { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A98; A100: n + 2 in Seg (n + 2) by A44, FINSEQ_1:1; A101: len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:59, XXREAL_0:2; then dom (h | (n + 2)) = Seg (n + 2) by FINSEQ_1:def_3; then x = (h | (n + 2)) /. ((n + 1) + 1) by A97, A100, FINSEQ_4:70; then x in LSeg ((h | (n + 2)),(n + 1)) by A101, A72, Th21; then A102: x in union { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A99, TARSKI:def_4; x in LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A97, RLTOPSP1:68; hence x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) by A102, XBOOLE_0:def_4; ::_thesis: verum end; then H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) = {(h /. (n + 2))} by TARSKI:def_1; then consider hh being Function of I[01],((TOP-REAL 2) | NE1) such that A103: hh is being_homeomorphism and A104: hh . 0 = f . 0 and A105: hh . 1 = f1 . 1 by A12, A13, A71, A68, A69, TOPMETR2:3; take hh ; ::_thesis: ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) ) thus ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) ) by A71, A70, A103, A104, A105; ::_thesis: verum end; h | 2 = h | (Seg 2) by FINSEQ_1:def_15; then A106: dom (h | 2) = (dom h) /\ (Seg 2) by RELAT_1:61 .= (Seg (len h)) /\ (Seg 2) by FINSEQ_1:def_3 .= Seg 2 by A2, FINSEQ_1:7 ; then A107: len (h | 2) = 1 + 1 by FINSEQ_1:def_3; then A108: 2 in Seg (len (h | 2)) by FINSEQ_1:1; A109: 1 in Seg (len (h | 2)) by A107, FINSEQ_1:1; now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__(LSeg_((h_|_2),i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_(h_|_2)_)__}__implies_x_=_LSeg_(h,1)_)_&_(_x_=_LSeg_(h,1)_implies_x_in__{__(LSeg_((h_|_2),i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_(h_|_2)_)__}__)_) let x be set ; ::_thesis: ( ( x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) & ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ) ) A110: h /. (1 + 1) = (h | 2) /. 2 by A106, A107, A108, FINSEQ_4:70; thus ( x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) ::_thesis: ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ) proof assume x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ; ::_thesis: x = LSeg (h,1) then consider i being Element of NAT such that A111: x = LSeg ((h | 2),i) and A112: 1 <= i and A113: i + 1 <= len (h | 2) ; i + 1 <= 1 + 1 by A106, A113, FINSEQ_1:def_3; then i <= 1 by XREAL_1:6; then A114: 1 = i by A112, XXREAL_0:1; A115: (h | 2) /. (1 + 1) = h /. (1 + 1) by A106, A107, A108, FINSEQ_4:70; (h | 2) /. 1 = h /. 1 by A106, A107, A109, FINSEQ_4:70; hence x = LSeg ((h /. 1),(h /. (1 + 1))) by A107, A111, A114, A115, Def3 .= LSeg (h,1) by A2, Def3 ; ::_thesis: verum end; assume x = LSeg (h,1) ; ::_thesis: x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } then A116: x = LSeg ((h /. 1),(h /. (1 + 1))) by A2, Def3; h /. 1 = (h | 2) /. 1 by A106, A107, A109, FINSEQ_4:70; then x = LSeg ((h | 2),1) by A107, A116, A110, Def3; hence x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } by A107; ::_thesis: verum end; then { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } = {(LSeg (h,1))} by TARSKI:def_1; then A117: H1( 0 ) = LSeg (h,1) by ZFMISC_1:25 .= LSeg ((h /. 1),(h /. (1 + 1))) by A2, Def3 ; A118: 1 + 1 in Seg (len h) by A2, FINSEQ_1:1; ( 1 <= 0 + 2 & 0 + 2 <= len h implies ex f being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. 1),(h /. (1 + 1))))) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) ) proof assume that 1 <= 0 + 2 and 0 + 2 <= len h ; ::_thesis: ex f being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. 1),(h /. (1 + 1))))) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) A119: 2 in dom h by A118, FINSEQ_1:def_3; 1 in dom h by A3, FINSEQ_1:def_3; then LSeg ((h /. 1),(h /. (1 + 1))) is_an_arc_of h /. 1,h /. (1 + 1) by A4, A119, Th9, PARTFUN2:10; hence ex f being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. 1),(h /. (1 + 1))))) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) by Def1; ::_thesis: verum end; then A120: S1[ 0 ] by A117; A121: for n being Nat holds S1[n] from NAT_1:sch_2(A120, A5); (len h) - 2 in NAT by A2, INT_1:5; then reconsider h1 = (len h) - 2 as Nat ; 1 <= h1 + 2 by NAT_1:12; then consider NE being non empty Subset of (TOP-REAL 2) such that A122: NE = H1(h1) and A123: ex f being Function of I[01],((TOP-REAL 2) | NE) st ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (h1 + 2) ) by A121; consider f being Function of I[01],((TOP-REAL 2) | NE) such that A124: f is being_homeomorphism and A125: f . 0 = h /. 1 and A126: f . 1 = h /. (h1 + 2) by A123; A127: h | (len h) = h | (Seg (len h)) by FINSEQ_1:def_15 .= h | (dom h) by FINSEQ_1:def_3 .= h by RELAT_1:68 ; then reconsider f = f as Function of I[01],((TOP-REAL 2) | (L~ h)) by A122; take f ; :: according to TOPREAL1:def_1 ::_thesis: ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (len h) ) thus f is being_homeomorphism by A122, A124, A127; ::_thesis: ( f . 0 = h /. 1 & f . 1 = h /. (len h) ) thus ( f . 0 = h /. 1 & f . 1 = h /. (len h) ) by A125, A126; ::_thesis: verum end; definition let P be Subset of (TOP-REAL 2); attrP is being_S-P_arc means :Def9: :: TOPREAL1:def 9 ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f ); end; :: deftheorem Def9 defines being_S-P_arc TOPREAL1:def_9_:_ for P being Subset of (TOP-REAL 2) holds ( P is being_S-P_arc iff ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P = L~ f ) ); theorem Th26: :: TOPREAL1:26 for P1 being Subset of (TOP-REAL 2) st P1 is being_S-P_arc holds P1 <> {} proof let P1 be Subset of (TOP-REAL 2); ::_thesis: ( P1 is being_S-P_arc implies P1 <> {} ) assume P1 is being_S-P_arc ; ::_thesis: P1 <> {} then consider f being FinSequence of (TOP-REAL 2) such that A1: f is being_S-Seq and A2: P1 = L~ f by Def9; len f >= 2 by A1, Def8; hence P1 <> {} by A2, Th23; ::_thesis: verum end; registration cluster being_S-P_arc -> non empty for Element of K10( the carrier of (TOP-REAL 2)); coherence for b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc holds not b1 is empty by Th26; end; theorem :: TOPREAL1:27 ex P1, P2 being non empty Subset of (TOP-REAL 2) st ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} ) proof consider f1, f2 being FinSequence of (TOP-REAL 2) such that A1: f1 is being_S-Seq and A2: f2 is being_S-Seq and A3: R^2-unit_square = (L~ f1) \/ (L~ f2) and A4: (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} and f1 /. 1 = |[0,0]| and f1 /. (len f1) = |[1,1]| and f2 /. 1 = |[0,0]| and f2 /. (len f2) = |[1,1]| by Th24; reconsider P1 = L~ f1, P2 = L~ f2 as non empty Subset of (TOP-REAL 2) by A4; take P1 ; ::_thesis: ex P2 being non empty Subset of (TOP-REAL 2) st ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} ) take P2 ; ::_thesis: ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} ) thus ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} ) by A1, A2, A3, A4, Def9; ::_thesis: verum end; theorem Th28: :: TOPREAL1:28 for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_S-P_arc implies ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 ) assume P is being_S-P_arc ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 then consider h being FinSequence of (TOP-REAL 2) such that A1: h is being_S-Seq and A2: P = L~ h by Def9; take h /. 1 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) st P is_an_arc_of h /. 1,p2 take h /. (len h) ; ::_thesis: P is_an_arc_of h /. 1,h /. (len h) thus P is_an_arc_of h /. 1,h /. (len h) by A1, A2, Th25; ::_thesis: verum end; theorem :: TOPREAL1:29 for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_S-P_arc implies ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism ) assume P is being_S-P_arc ; ::_thesis: ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism then consider p1, p2 being Point of (TOP-REAL 2) such that A1: P is_an_arc_of p1,p2 by Th28; ex f being Function of I[01],((TOP-REAL 2) | P) st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, Def1; hence ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism ; ::_thesis: verum end; scheme :: TOPREAL1:sch 2 TRSubsetEx{ F1() -> Nat, P1[ set ] } : ex A being Subset of (TOP-REAL F1()) st for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in the carrier of (TOP-REAL F1()) & P1[x] ) ) from XBOOLE_0:sch_1(); A c= the carrier of (TOP-REAL F1()) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of (TOP-REAL F1()) ) assume x in A ; ::_thesis: x in the carrier of (TOP-REAL F1()) hence x in the carrier of (TOP-REAL F1()) by A1; ::_thesis: verum end; then reconsider A = A as Subset of (TOP-REAL F1()) ; take A ; ::_thesis: for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) thus for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) by A1; ::_thesis: verum end; scheme :: TOPREAL1:sch 3 TRSubsetUniq{ F1() -> Nat, P1[ set ] } : for A, B being Subset of (TOP-REAL F1()) st ( for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) ) & ( for p being Point of (TOP-REAL F1()) holds ( p in B iff P1[p] ) ) holds A = B proof let A, B be Subset of (TOP-REAL F1()); ::_thesis: ( ( for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) ) & ( for p being Point of (TOP-REAL F1()) holds ( p in B iff P1[p] ) ) implies A = B ) assume that A1: for p being Point of (TOP-REAL F1()) holds ( p in A iff P1[p] ) and A2: for p being Point of (TOP-REAL F1()) holds ( p in B iff P1[p] ) ; ::_thesis: A = B hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: B c= A let x be set ; ::_thesis: ( x in A implies x in B ) assume A3: x in A ; ::_thesis: x in B then P1[x] by A1; hence x in B by A2, A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A ) assume A4: x in B ; ::_thesis: x in A then P1[x] by A2; hence x in A by A1, A4; ::_thesis: verum end; definition let p be Point of (TOP-REAL 2); func north_halfline p -> Subset of (TOP-REAL 2) means :Def10: :: TOPREAL1:def 10 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 = p `1 & x `2 >= p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 >= p `2 ) ) proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 >= p `2 ); thus ex IT being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) holds b1 = b2 proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 >= p `2 ); thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b iff S1[x] ) ) holds a = b from TOPREAL1:sch_3(); ::_thesis: verum end; func east_halfline p -> Subset of (TOP-REAL 2) means :Def11: :: TOPREAL1:def 11 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 >= p `1 & x `2 = p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 >= p `1 & x `2 = p `2 ) ) proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 >= p `1 & $1 `2 = p `2 ); thus ex IT being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) holds b1 = b2 proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 >= p `1 & $1 `2 = p `2 ); thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b iff S1[x] ) ) holds a = b from TOPREAL1:sch_3(); ::_thesis: verum end; func south_halfline p -> Subset of (TOP-REAL 2) means :Def12: :: TOPREAL1:def 12 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 = p `1 & x `2 <= p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 <= p `2 ) ) proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 <= p `2 ); thus ex IT being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) holds b1 = b2 proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 <= p `2 ); thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b iff S1[x] ) ) holds a = b from TOPREAL1:sch_3(); ::_thesis: verum end; func west_halfline p -> Subset of (TOP-REAL 2) means :Def13: :: TOPREAL1:def 13 for x being Point of (TOP-REAL 2) holds ( x in it iff ( x `1 <= p `1 & x `2 = p `2 ) ); existence ex b1 being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 <= p `1 & x `2 = p `2 ) ) proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 <= p `1 & $1 `2 = p `2 ); thus ex IT being Subset of (TOP-REAL 2) st for x being Point of (TOP-REAL 2) holds ( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum end; uniqueness for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in b1 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) holds b1 = b2 proof defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 <= p `1 & $1 `2 = p `2 ); thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds ( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds ( x in b iff S1[x] ) ) holds a = b from TOPREAL1:sch_3(); ::_thesis: verum end; end; :: deftheorem Def10 defines north_halfline TOPREAL1:def_10_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = north_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ); :: deftheorem Def11 defines east_halfline TOPREAL1:def_11_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = east_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ); :: deftheorem Def12 defines south_halfline TOPREAL1:def_12_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = south_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ); :: deftheorem Def13 defines west_halfline TOPREAL1:def_13_:_ for p being Point of (TOP-REAL 2) for b2 being Subset of (TOP-REAL 2) holds ( b2 = west_halfline p iff for x being Point of (TOP-REAL 2) holds ( x in b2 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ); theorem :: TOPREAL1:30 for p being Point of (TOP-REAL 2) holds north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } proof let p be Point of (TOP-REAL 2); ::_thesis: north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } set A = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } c= north_halfline p let x be set ; ::_thesis: ( x in north_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } ) assume A1: x in north_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 >= p `2 by A1, Def10; q `1 = p `1 by A1, Def10; hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } by A2; ::_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) : ( q `1 = p `1 & q `2 >= p `2 ) } or x in north_halfline p ) assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } ; ::_thesis: x in north_halfline p then ex q being Point of (TOP-REAL 2) st ( x = q & q `1 = p `1 & q `2 >= p `2 ) ; hence x in north_halfline p by Def10; ::_thesis: verum end; theorem Th31: :: TOPREAL1:31 for p being Point of (TOP-REAL 2) holds north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } proof let p be Point of (TOP-REAL 2); ::_thesis: north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } set A = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[(p `1),r]| where r is Element of REAL : r >= p `2 } c= north_halfline p let x be set ; ::_thesis: ( x in north_halfline p implies x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } ) assume A1: x in north_halfline p ; ::_thesis: x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 >= p `2 by A1, Def10; A3: q = |[(q `1),(q `2)]| by EUCLID:53; q `1 = p `1 by A1, Def10; hence x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } by A2, A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } or x in north_halfline p ) assume x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } ; ::_thesis: x in north_halfline p then consider r being Element of REAL such that A4: x = |[(p `1),r]| and A5: r >= p `2 ; reconsider q = x as Point of (TOP-REAL 2) by A4; A6: q `2 = r by A4, EUCLID:52; q `1 = p `1 by A4, EUCLID:52; hence x in north_halfline p by A5, A6, Def10; ::_thesis: verum end; theorem :: TOPREAL1:32 for p being Point of (TOP-REAL 2) holds east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } proof let p be Point of (TOP-REAL 2); ::_thesis: east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } set A = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } c= east_halfline p let x be set ; ::_thesis: ( x in east_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } ) assume A1: x in east_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 = p `2 by A1, Def11; q `1 >= p `1 by A1, Def11; hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } by A2; ::_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) : ( q `1 >= p `1 & q `2 = p `2 ) } or x in east_halfline p ) assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } ; ::_thesis: x in east_halfline p then ex q being Point of (TOP-REAL 2) st ( x = q & q `1 >= p `1 & q `2 = p `2 ) ; hence x in east_halfline p by Def11; ::_thesis: verum end; theorem Th33: :: TOPREAL1:33 for p being Point of (TOP-REAL 2) holds east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } proof let p be Point of (TOP-REAL 2); ::_thesis: east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } set A = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } c= east_halfline p let x be set ; ::_thesis: ( x in east_halfline p implies x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } ) assume A1: x in east_halfline p ; ::_thesis: x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 = p `2 by A1, Def11; A3: q = |[(q `1),(q `2)]| by EUCLID:53; q `1 >= p `1 by A1, Def11; hence x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } by A2, A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } or x in east_halfline p ) assume x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } ; ::_thesis: x in east_halfline p then consider r being Element of REAL such that A4: x = |[r,(p `2)]| and A5: r >= p `1 ; reconsider q = x as Point of (TOP-REAL 2) by A4; A6: q `2 = p `2 by A4, EUCLID:52; q `1 = r by A4, EUCLID:52; hence x in east_halfline p by A5, A6, Def11; ::_thesis: verum end; theorem :: TOPREAL1:34 for p being Point of (TOP-REAL 2) holds south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } proof let p be Point of (TOP-REAL 2); ::_thesis: south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } set A = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } c= south_halfline p let x be set ; ::_thesis: ( x in south_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } ) assume A1: x in south_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 <= p `2 by A1, Def12; q `1 = p `1 by A1, Def12; hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } by A2; ::_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) : ( q `1 = p `1 & q `2 <= p `2 ) } or x in south_halfline p ) assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } ; ::_thesis: x in south_halfline p then ex q being Point of (TOP-REAL 2) st ( x = q & q `1 = p `1 & q `2 <= p `2 ) ; hence x in south_halfline p by Def12; ::_thesis: verum end; theorem Th35: :: TOPREAL1:35 for p being Point of (TOP-REAL 2) holds south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } proof let p be Point of (TOP-REAL 2); ::_thesis: south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } set A = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[(p `1),r]| where r is Element of REAL : r <= p `2 } c= south_halfline p let x be set ; ::_thesis: ( x in south_halfline p implies x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } ) assume A1: x in south_halfline p ; ::_thesis: x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 <= p `2 by A1, Def12; A3: q = |[(q `1),(q `2)]| by EUCLID:53; q `1 = p `1 by A1, Def12; hence x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } by A2, A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } or x in south_halfline p ) assume x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } ; ::_thesis: x in south_halfline p then consider r being Element of REAL such that A4: x = |[(p `1),r]| and A5: r <= p `2 ; reconsider q = x as Point of (TOP-REAL 2) by A4; A6: q `2 = r by A4, EUCLID:52; q `1 = p `1 by A4, EUCLID:52; hence x in south_halfline p by A5, A6, Def12; ::_thesis: verum end; theorem :: TOPREAL1:36 for p being Point of (TOP-REAL 2) holds west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } proof let p be Point of (TOP-REAL 2); ::_thesis: west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } set A = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } c= west_halfline p let x be set ; ::_thesis: ( x in west_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } ) assume A1: x in west_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 = p `2 by A1, Def13; q `1 <= p `1 by A1, Def13; hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } by A2; ::_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) : ( q `1 <= p `1 & q `2 = p `2 ) } or x in west_halfline p ) assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } ; ::_thesis: x in west_halfline p then ex q being Point of (TOP-REAL 2) st ( x = q & q `1 <= p `1 & q `2 = p `2 ) ; hence x in west_halfline p by Def13; ::_thesis: verum end; theorem Th37: :: TOPREAL1:37 for p being Point of (TOP-REAL 2) holds west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } proof let p be Point of (TOP-REAL 2); ::_thesis: west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } set A = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } ; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } c= west_halfline p let x be set ; ::_thesis: ( x in west_halfline p implies x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } ) assume A1: x in west_halfline p ; ::_thesis: x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } then reconsider q = x as Point of (TOP-REAL 2) ; A2: q `2 = p `2 by A1, Def13; A3: q = |[(q `1),(q `2)]| by EUCLID:53; q `1 <= p `1 by A1, Def13; hence x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } by A2, A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } or x in west_halfline p ) assume x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } ; ::_thesis: x in west_halfline p then consider r being Element of REAL such that A4: x = |[r,(p `2)]| and A5: r <= p `1 ; reconsider q = x as Point of (TOP-REAL 2) by A4; A6: q `2 = p `2 by A4, EUCLID:52; q `1 = r by A4, EUCLID:52; hence x in west_halfline p by A5, A6, Def13; ::_thesis: verum end; registration let p be Point of (TOP-REAL 2); cluster north_halfline p -> non empty ; coherence not north_halfline p is empty proof north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } by Th31; then |[(p `1),(p `2)]| in north_halfline p ; hence not north_halfline p is empty ; ::_thesis: verum end; cluster east_halfline p -> non empty ; coherence not east_halfline p is empty proof east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } by Th33; then |[(p `1),(p `2)]| in east_halfline p ; hence not east_halfline p is empty ; ::_thesis: verum end; cluster south_halfline p -> non empty ; coherence not south_halfline p is empty proof south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } by Th35; then |[(p `1),(p `2)]| in south_halfline p ; hence not south_halfline p is empty ; ::_thesis: verum end; cluster west_halfline p -> non empty ; coherence not west_halfline p is empty proof west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } by Th37; then |[(p `1),(p `2)]| in west_halfline p ; hence not west_halfline p is empty ; ::_thesis: verum end; end; theorem :: TOPREAL1:38 for p being Point of (TOP-REAL 2) holds ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) A1: p `2 = p `2 ; p `1 <= p `1 ; hence ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) by A1, Def10, Def11, Def12, Def13; ::_thesis: verum end;