:: TOPREAL5 semantic presentation begin Lm1: for X, Y, Z being non empty TopSpace for f being continuous Function of X,Y for g being continuous Function of Y,Z holds g * f is continuous Function of X,Z ; theorem Th1: :: TOPREAL5:1 for X being non empty TopSpace for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds not A is connected proof let X be non empty TopSpace; ::_thesis: for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds not A is connected let A, B1, B2 be Subset of X; ::_thesis: ( B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 implies not A is connected ) assume that A1: ( B1 is open & B2 is open & B1 meets A ) and A2: B2 meets A and A3: A c= B1 \/ B2 and A4: B1 misses B2 ; ::_thesis: not A is connected reconsider C1 = B1 /\ A, C2 = B2 /\ A as Subset of X ; A5: A = (B1 \/ B2) /\ A by A3, XBOOLE_1:28 .= C1 \/ C2 by XBOOLE_1:23 ; A6: C2 <> {} by A2, XBOOLE_0:def_7; A7: ( A is connected iff for P, Q being Subset of X st A = P \/ Q & P,Q are_separated & not P = {} X holds Q = {} X ) by CONNSP_1:15; A8: ( C1 c= B1 & C2 c= B2 ) by XBOOLE_1:17; ( B1,B2 are_separated & C1 <> {} ) by A1, A4, TSEP_1:37, XBOOLE_0:def_7; hence not A is connected by A7, A5, A8, A6, CONNSP_1:7; ::_thesis: verum end; theorem Th2: :: TOPREAL5:2 for ra, rb being real number st ra <= rb holds [#] (Closed-Interval-TSpace (ra,rb)) is connected proof let ra, rb be real number ; ::_thesis: ( ra <= rb implies [#] (Closed-Interval-TSpace (ra,rb)) is connected ) assume ra <= rb ; ::_thesis: [#] (Closed-Interval-TSpace (ra,rb)) is connected then Closed-Interval-TSpace (ra,rb) is connected by TREAL_1:20; hence [#] (Closed-Interval-TSpace (ra,rb)) is connected by CONNSP_1:27; ::_thesis: verum end; theorem Th3: :: TOPREAL5:3 for A being Subset of R^1 for a being real number st not a in A & ex b, d being real number st ( b in A & d in A & b < a & a < d ) holds not A is connected proof let A be Subset of R^1; ::_thesis: for a being real number st not a in A & ex b, d being real number st ( b in A & d in A & b < a & a < d ) holds not A is connected let a be real number ; ::_thesis: ( not a in A & ex b, d being real number st ( b in A & d in A & b < a & a < d ) implies not A is connected ) assume that A1: not a in A and A2: ex b, d being real number st ( b in A & d in A & b < a & a < d ) ; ::_thesis: not A is connected consider b, d being real number such that A3: b in A and A4: d in A and A5: b < a and A6: a < d by A2; set B2 = { s where s is Element of REAL : s > a } ; set B1 = { r where r is Element of REAL : r < a } ; A7: A c= { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } ) assume A8: x in A ; ::_thesis: x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } then reconsider r = x as Real by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; ( r < a or a < r ) by A1, A8, XXREAL_0:1; then ( r in { r where r is Element of REAL : r < a } or r in { s where s is Element of REAL : s > a } ) ; hence x in { r where r is Element of REAL : r < a } \/ { s where s is Element of REAL : s > a } by XBOOLE_0:def_3; ::_thesis: verum end; { s where s is Element of REAL : s > a } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { s where s is Element of REAL : s > a } or x in REAL ) assume x in { s where s is Element of REAL : s > a } ; ::_thesis: x in REAL then ex r being Element of REAL st ( r = x & r > a ) ; hence x in REAL ; ::_thesis: verum end; then reconsider C2 = { s where s is Element of REAL : s > a } as Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; { r where r is Element of REAL : r < a } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Element of REAL : r < a } or x in REAL ) assume x in { r where r is Element of REAL : r < a } ; ::_thesis: x in REAL then ex r being Element of REAL st ( r = x & r < a ) ; hence x in REAL ; ::_thesis: verum end; then reconsider C1 = { r where r is Element of REAL : r < a } as Subset of R^1 by METRIC_1:def_13, TOPMETR:12, TOPMETR:def_6; A9: now__::_thesis:_not__{__r_where_r_is_Element_of_REAL_:_r_<_a__}__meets__{__s_where_s_is_Element_of_REAL_:_s_>_a__}_ assume { r where r is Element of REAL : r < a } meets { s where s is Element of REAL : s > a } ; ::_thesis: contradiction then consider x being set such that A10: x in { r where r is Element of REAL : r < a } /\ { s where s is Element of REAL : s > a } by XBOOLE_0:4; x in { s where s is Element of REAL : s > a } by A10, XBOOLE_0:def_4; then A11: ex r2 being Element of REAL st ( r2 = x & r2 > a ) ; x in { r where r is Element of REAL : r < a } by A10, XBOOLE_0:def_4; then ex r1 being Element of REAL st ( r1 = x & r1 < a ) ; hence contradiction by A11; ::_thesis: verum end; reconsider r1 = d as Element of REAL by XREAL_0:def_1; r1 in { s where s is Element of REAL : s > a } by A6; then d in { s where s is Element of REAL : s > a } /\ A by A4, XBOOLE_0:def_4; then A12: { s where s is Element of REAL : s > a } meets A by XBOOLE_0:4; reconsider r = b as Element of REAL by XREAL_0:def_1; r in { r where r is Element of REAL : r < a } by A5; then b in { r where r is Element of REAL : r < a } /\ A by A3, XBOOLE_0:def_4; then A13: { r where r is Element of REAL : r < a } meets A by XBOOLE_0:4; ( C1 is open & C2 is open ) by JORDAN2B:24, JORDAN2B:25; hence not A is connected by A9, A13, A12, A7, Th1; ::_thesis: verum end; theorem :: TOPREAL5:4 for X being non empty TopSpace for xa, xb being Point of X for a, b, d being Real for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds ex xc being Point of X st f . xc = d proof let X be non empty TopSpace; ::_thesis: for xa, xb being Point of X for a, b, d being Real for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds ex xc being Point of X st f . xc = d let xa, xb be Point of X; ::_thesis: for a, b, d being Real for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds ex xc being Point of X st f . xc = d let a, b, d be Real; ::_thesis: for f being continuous Function of X,R^1 st X is connected & f . xa = a & f . xb = b & a <= d & d <= b holds ex xc being Point of X st f . xc = d let f be continuous Function of X,R^1; ::_thesis: ( X is connected & f . xa = a & f . xb = b & a <= d & d <= b implies ex xc being Point of X st f . xc = d ) assume that A1: X is connected and A2: ( f . xa = a & f . xb = b ) and A3: ( a <= d & d <= b ) ; ::_thesis: ex xc being Point of X st f . xc = d now__::_thesis:_(_not_a_=_d_&_not_d_=_b_implies_ex_xc_being_Point_of_X_st_f_._xc_=_d_) assume ( not a = d & not d = b ) ; ::_thesis: ex xc being Point of X st f . xc = d then A4: ( a < d & d < b ) by A3, XXREAL_0:1; now__::_thesis:_ex_rc_being_Point_of_X_st_f_._rc_=_d assume A5: for rc being Point of X holds not f . rc = d ; ::_thesis: contradiction A6: now__::_thesis:_not_d_in_f_.:_([#]_X) assume d in f .: ([#] X) ; ::_thesis: contradiction then ex x being set st ( x in the carrier of X & x in [#] X & d = f . x ) by FUNCT_2:64; hence contradiction by A5; ::_thesis: verum end; dom f = the carrier of X by FUNCT_2:def_1; then A7: ( a in f .: ([#] X) & b in f .: ([#] X) ) by A2, FUNCT_1:def_6; [#] X is connected by A1, CONNSP_1:27; hence contradiction by A4, A6, A7, Th3, TOPS_2:61; ::_thesis: verum end; hence ex xc being Point of X st f . xc = d ; ::_thesis: verum end; hence ex xc being Point of X st f . xc = d by A2; ::_thesis: verum end; theorem :: TOPREAL5:5 for X being non empty TopSpace for xa, xb being Point of X for B being Subset of X for a, b, d being Real for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds ex xc being Point of X st ( xc in B & f . xc = d ) proof let X be non empty TopSpace; ::_thesis: for xa, xb being Point of X for B being Subset of X for a, b, d being Real for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds ex xc being Point of X st ( xc in B & f . xc = d ) let xa, xb be Point of X; ::_thesis: for B being Subset of X for a, b, d being Real for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds ex xc being Point of X st ( xc in B & f . xc = d ) let B be Subset of X; ::_thesis: for a, b, d being Real for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds ex xc being Point of X st ( xc in B & f . xc = d ) let a, b, d be Real; ::_thesis: for f being continuous Function of X,R^1 st B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B holds ex xc being Point of X st ( xc in B & f . xc = d ) let f be continuous Function of X,R^1; ::_thesis: ( B is connected & f . xa = a & f . xb = b & a <= d & d <= b & xa in B & xb in B implies ex xc being Point of X st ( xc in B & f . xc = d ) ) assume that A1: B is connected and A2: ( f . xa = a & f . xb = b ) and A3: ( a <= d & d <= b ) and A4: ( xa in B & xb in B ) ; ::_thesis: ex xc being Point of X st ( xc in B & f . xc = d ) now__::_thesis:_(_not_a_=_d_&_not_d_=_b_implies_ex_xc_being_Point_of_X_st_ (_xc_in_B_&_f_._xc_=_d_)_) assume ( not a = d & not d = b ) ; ::_thesis: ex xc being Point of X st ( xc in B & f . xc = d ) then A5: ( a < d & d < b ) by A3, XXREAL_0:1; now__::_thesis:_ex_rc_being_Point_of_X_st_ (_rc_in_B_&_f_._rc_=_d_) assume A6: for rc being Point of X holds ( not rc in B or not f . rc = d ) ; ::_thesis: contradiction A7: now__::_thesis:_not_d_in_f_.:_B assume d in f .: B ; ::_thesis: contradiction then ex x being set st ( x in the carrier of X & x in B & d = f . x ) by FUNCT_2:64; hence contradiction by A6; ::_thesis: verum end; dom f = the carrier of X by FUNCT_2:def_1; then ( a in f .: B & b in f .: B ) by A2, A4, FUNCT_1:def_6; hence contradiction by A1, A5, A7, Th3, TOPS_2:61; ::_thesis: verum end; hence ex xc being Point of X st ( xc in B & f . xc = d ) ; ::_thesis: verum end; hence ex xc being Point of X st ( xc in B & f . xc = d ) by A2, A4; ::_thesis: verum end; theorem Th6: :: TOPREAL5:6 for ra, rb, a, b being real number st ra < rb holds for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a < d & d < b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) proof let ra, rb, a, b be real number ; ::_thesis: ( ra < rb implies for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a < d & d < b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) ) assume A1: ra < rb ; ::_thesis: for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a < d & d < b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) let f be continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1; ::_thesis: for d being real number st f . ra = a & f . rb = b & a < d & d < b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) let d be real number ; ::_thesis: ( f . ra = a & f . rb = b & a < d & d < b implies ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) ) assume that A2: f . ra = a and A3: f . rb = b and A4: a < d and A5: d < b ; ::_thesis: ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) now__::_thesis:_ex_rc_being_Element_of_REAL_st_ (_f_._rc_=_d_&_ra_<_rc_&_rc_<_rb_) reconsider C = f .: ([#] (Closed-Interval-TSpace (ra,rb))) as Subset of R^1 ; A6: dom f = the carrier of (Closed-Interval-TSpace (ra,rb)) by FUNCT_2:def_1; A7: the carrier of (Closed-Interval-TSpace (ra,rb)) = [.ra,rb.] by A1, TOPMETR:18; then rb in [#] (Closed-Interval-TSpace (ra,rb)) by A1, XXREAL_1:1; then A8: b in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A3, A6, FUNCT_1:def_6; assume A9: for rc being Element of REAL holds ( not f . rc = d or not ra < rc or not rc < rb ) ; ::_thesis: contradiction A10: now__::_thesis:_not_d_in_f_.:_([#]_(Closed-Interval-TSpace_(ra,rb))) assume d in f .: ([#] (Closed-Interval-TSpace (ra,rb))) ; ::_thesis: contradiction then consider x being set such that A11: x in the carrier of (Closed-Interval-TSpace (ra,rb)) and x in [#] (Closed-Interval-TSpace (ra,rb)) and A12: d = f . x by FUNCT_2:64; reconsider r = x as Real by A7, A11; r <= rb by A7, A11, XXREAL_1:1; then A13: r < rb by A3, A5, A12, XXREAL_0:1; ra <= r by A7, A11, XXREAL_1:1; then ra < r by A2, A4, A12, XXREAL_0:1; hence contradiction by A9, A12, A13; ::_thesis: verum end; ra in [#] (Closed-Interval-TSpace (ra,rb)) by A1, A7, XXREAL_1:1; then a in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A2, A6, FUNCT_1:def_6; then not C is connected by A4, A5, A10, A8, Th3; hence contradiction by A1, Th2, TOPS_2:61; ::_thesis: verum end; hence ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) ; ::_thesis: verum end; theorem Th7: :: TOPREAL5:7 for ra, rb, a, b being real number st ra < rb holds for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a > d & d > b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) proof let ra, rb, a, b be real number ; ::_thesis: ( ra < rb implies for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a > d & d > b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) ) assume A1: ra < rb ; ::_thesis: for f being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for d being real number st f . ra = a & f . rb = b & a > d & d > b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) then A2: the carrier of (Closed-Interval-TSpace (ra,rb)) = [.ra,rb.] by TOPMETR:18; let f be continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1; ::_thesis: for d being real number st f . ra = a & f . rb = b & a > d & d > b holds ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) let d be real number ; ::_thesis: ( f . ra = a & f . rb = b & a > d & d > b implies ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) ) assume that A3: f . ra = a and A4: f . rb = b and A5: a > d and A6: d > b ; ::_thesis: ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) A7: dom f = the carrier of (Closed-Interval-TSpace (ra,rb)) by FUNCT_2:def_1; A8: [#] (Closed-Interval-TSpace (ra,rb)) is connected by A1, Th2; now__::_thesis:_ex_rc_being_Element_of_REAL_st_ (_ra_<_rc_&_rc_<_rb_&_not_f_._rc_<>_d_) assume A9: for rc being Element of REAL st ra < rc & rc < rb holds f . rc <> d ; ::_thesis: contradiction A10: now__::_thesis:_not_d_in_f_.:_([#]_(Closed-Interval-TSpace_(ra,rb))) assume d in f .: ([#] (Closed-Interval-TSpace (ra,rb))) ; ::_thesis: contradiction then consider x being set such that A11: x in dom f and x in [#] (Closed-Interval-TSpace (ra,rb)) and A12: d = f . x by FUNCT_1:def_6; x in [.ra,rb.] by A2, A11; then reconsider r = x as Real ; r <= rb by A2, A11, XXREAL_1:1; then A13: rb > r by A4, A6, A12, XXREAL_0:1; ra <= r by A2, A11, XXREAL_1:1; then ra < r by A3, A5, A12, XXREAL_0:1; hence contradiction by A9, A12, A13; ::_thesis: verum end; rb in [.ra,rb.] by A1, XXREAL_1:1; then A14: b in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A4, A2, A7, FUNCT_1:def_6; ra in [.ra,rb.] by A1, XXREAL_1:1; then a in f .: ([#] (Closed-Interval-TSpace (ra,rb))) by A3, A2, A7, FUNCT_1:def_6; hence contradiction by A5, A6, A8, A10, A14, Th3, TOPS_2:61; ::_thesis: verum end; hence ex rc being Element of REAL st ( f . rc = d & ra < rc & rc < rb ) ; ::_thesis: verum end; theorem :: TOPREAL5:8 for ra, rb being real number for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) proof let ra, rb be real number ; ::_thesis: for g being continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1 for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) let g be continuous Function of (Closed-Interval-TSpace (ra,rb)),R^1; ::_thesis: for s1, s2 being real number st ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb holds ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) let s1, s2 be real number ; ::_thesis: ( ra < rb & s1 * s2 < 0 & s1 = g . ra & s2 = g . rb implies ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) ) assume that A1: ra < rb and A2: s1 * s2 < 0 ; ::_thesis: ( not s1 = g . ra or not s2 = g . rb or ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) ) ( ( s1 > 0 & s2 < 0 ) or ( s1 < 0 & s2 > 0 ) ) by A2, XREAL_1:133; hence ( not s1 = g . ra or not s2 = g . rb or ex r1 being Element of REAL st ( g . r1 = 0 & ra < r1 & r1 < rb ) ) by A1, Th6, Th7; ::_thesis: verum end; theorem Th9: :: TOPREAL5:9 for g being Function of I[01],R^1 for s1, s2 being real number st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds ex r1 being Element of REAL st ( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) proof let g be Function of I[01],R^1; ::_thesis: for s1, s2 being real number st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds ex r1 being Element of REAL st ( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) let s1, s2 be real number ; ::_thesis: ( g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 implies ex r1 being Element of REAL st ( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) ) assume that A1: g is continuous and A2: g . 0 <> g . 1 and A3: ( s1 = g . 0 & s2 = g . 1 ) ; ::_thesis: ex r1 being Element of REAL st ( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) now__::_thesis:_(_(_s1_<_s2_&_ex_rc_being_Element_of_REAL_st_ (_g_._rc_=_(s1_+_s2)_/_2_&_0_<_rc_&_rc_<_1_)_)_or_(_s2_<_s1_&_ex_rc_being_Element_of_REAL_st_ (_g_._rc_=_(s1_+_s2)_/_2_&_0_<_rc_&_rc_<_1_)_)_) percases ( s1 < s2 or s2 < s1 ) by A2, A3, XXREAL_0:1; case s1 < s2 ; ::_thesis: ex rc being Element of REAL st ( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) then ( s1 < (s1 + s2) / 2 & (s1 + s2) / 2 < s2 ) by XREAL_1:226; hence ex rc being Element of REAL st ( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) by A1, A3, Th6, TOPMETR:20; ::_thesis: verum end; case s2 < s1 ; ::_thesis: ex rc being Element of REAL st ( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) then ( s2 < (s1 + s2) / 2 & (s1 + s2) / 2 < s1 ) by XREAL_1:226; hence ex rc being Element of REAL st ( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) by A1, A3, Th7, TOPMETR:20; ::_thesis: verum end; end; end; hence ex r1 being Element of REAL st ( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) ; ::_thesis: verum end; begin theorem Th10: :: TOPREAL5:10 for f being Function of (TOP-REAL 2),R^1 st f = proj1 holds f is continuous proof let f be Function of (TOP-REAL 2),R^1; ::_thesis: ( f = proj1 implies f is continuous ) assume f = proj1 ; ::_thesis: f is continuous then ( 1 in Seg 2 & ( for p being Element of (TOP-REAL 2) holds f . p = p /. 1 ) ) by FINSEQ_1:1, JORDAN2B:30; hence f is continuous by JORDAN2B:18; ::_thesis: verum end; theorem Th11: :: TOPREAL5:11 for f being Function of (TOP-REAL 2),R^1 st f = proj2 holds f is continuous proof let f be Function of (TOP-REAL 2),R^1; ::_thesis: ( f = proj2 implies f is continuous ) assume f = proj2 ; ::_thesis: f is continuous then ( 2 in Seg 2 & ( for p being Element of (TOP-REAL 2) holds f . p = p /. 2 ) ) by FINSEQ_1:1, JORDAN2B:30; hence f is continuous by JORDAN2B:18; ::_thesis: verum end; theorem Th12: :: TOPREAL5:12 for P being non empty Subset of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = g . r ) ) proof reconsider rj = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17; let P be non empty Subset of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = g . r ) ) let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: ( f is continuous implies ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = g . r ) ) ) assume A1: f is continuous ; ::_thesis: ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = g . r ) ) reconsider f1 = f as Function ; set h = (proj1 | P) * f; A2: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; then A3: rng f1 c= P by RELAT_1:def_19; rj is continuous Function of (TOP-REAL 2),R^1 by Th10; then rj | ((TOP-REAL 2) | P) is continuous Function of ((TOP-REAL 2) | P),R^1 ; then rj | P is continuous Function of ((TOP-REAL 2) | P),R^1 by A2, TMAP_1:def_3; then reconsider h2 = (proj1 | P) * f as continuous Function of I[01],R^1 by A1, Lm1; take h2 ; ::_thesis: ( h2 is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = h2 . r ) ) thus h2 is continuous ; ::_thesis: for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = h2 . r let r be Real; ::_thesis: for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `1 = h2 . r let q be Point of (TOP-REAL 2); ::_thesis: ( r in the carrier of I[01] & q = f . r implies q `1 = h2 . r ) assume that A4: r in the carrier of I[01] and A5: q = f . r ; ::_thesis: q `1 = h2 . r A6: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; A7: r in dom f1 by A4, FUNCT_2:def_1; then f1 . r in rng f1 by FUNCT_1:def_3; then A8: q in (dom proj1) /\ P by A5, A3, A6, XBOOLE_0:def_4; thus h2 . r = (proj1 | P) . q by A5, A7, FUNCT_1:13 .= proj1 . q by A8, FUNCT_1:48 .= q `1 by PSCOMP_1:def_5 ; ::_thesis: verum end; theorem Th13: :: TOPREAL5:13 for P being non empty Subset of (TOP-REAL 2) for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = g . r ) ) proof reconsider rj = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17; let P be non empty Subset of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P) st f is continuous holds ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = g . r ) ) let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: ( f is continuous implies ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = g . r ) ) ) assume A1: f is continuous ; ::_thesis: ex g being Function of I[01],R^1 st ( g is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = g . r ) ) reconsider f1 = f as Function ; set h = (proj2 | P) * f; A2: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def_5; then A3: rng f1 c= P by RELAT_1:def_19; rj is continuous by Th11; then rj | ((TOP-REAL 2) | P) is continuous Function of ((TOP-REAL 2) | P),R^1 ; then rj | P is continuous Function of ((TOP-REAL 2) | P),R^1 by A2, TMAP_1:def_3; then reconsider h2 = (proj2 | P) * f as continuous Function of I[01],R^1 by A1, Lm1; take h2 ; ::_thesis: ( h2 is continuous & ( for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = h2 . r ) ) thus h2 is continuous ; ::_thesis: for r being Element of REAL for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = h2 . r let r be Real; ::_thesis: for q being Point of (TOP-REAL 2) st r in the carrier of I[01] & q = f . r holds q `2 = h2 . r let q be Point of (TOP-REAL 2); ::_thesis: ( r in the carrier of I[01] & q = f . r implies q `2 = h2 . r ) assume that A4: r in the carrier of I[01] and A5: q = f . r ; ::_thesis: q `2 = h2 . r A6: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; A7: r in dom f1 by A4, FUNCT_2:def_1; then f1 . r in rng f1 by FUNCT_1:def_3; then A8: q in (dom proj2) /\ P by A5, A3, A6, XBOOLE_0:def_4; thus h2 . r = (proj2 | P) . q by A5, A7, FUNCT_1:13 .= proj2 . q by A8, FUNCT_1:48 .= q `2 by PSCOMP_1:def_6 ; ::_thesis: verum end; theorem Th14: :: TOPREAL5:14 for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `2 = r ) proof let P be non empty Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `2 = r ) ) assume A1: P is being_simple_closed_curve ; ::_thesis: for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `2 = r ) now__::_thesis:_for_r0_being_real_number_ex_p_being_Point_of_(TOP-REAL_2)_st_ (_p_in_P_&_not_p_`2_=_r0_) A2: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128; given r0 being real number such that A3: for p being Point of (TOP-REAL 2) st p in P holds p `2 = r0 ; ::_thesis: contradiction consider p1, p2 being Point of (TOP-REAL 2), P1, P2 being non empty Subset of (TOP-REAL 2) such that A4: p1 <> p2 and A5: p1 in P and A6: p2 in P and A7: P1 is_an_arc_of p1,p2 and A8: P2 is_an_arc_of p1,p2 and A9: P = P1 \/ P2 and A10: P1 /\ P2 = {p1,p2} by A1, TOPREAL2:6; A11: p1 `2 = r0 by A3, A5; A12: p2 `2 = r0 by A3, A6; then A13: p1 `2 = p2 `2 by A3, A5; A14: now__::_thesis:_not_p1_`1_=_p2_`1 assume p1 `1 = p2 `1 ; ::_thesis: contradiction then p1 = |[(p2 `1),(p2 `2)]| by A13, EUCLID:53; hence contradiction by A4, EUCLID:53; ::_thesis: verum end; consider f2 being Function of I[01],((TOP-REAL 2) | P2) such that A15: f2 is being_homeomorphism and A16: f2 . 0 = p1 and A17: f2 . 1 = p2 by A8, TOPREAL1:def_1; f2 is continuous by A15, TOPS_2:def_5; then consider g2 being Function of I[01],R^1 such that A18: g2 is continuous and A19: for r being Element of REAL for q2 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q2 = f2 . r holds q2 `1 = g2 . r by Th12; A20: [#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def_5; 1 in {0,1} by TARSKI:def_2; then A21: 1 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3; then A22: p2 `1 = g2 . 1 by A17, A19; 0 in {0,1} by TARSKI:def_2; then A23: 0 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3; then p1 `1 = g2 . 0 by A16, A19; then consider r2 being Element of REAL such that A24: ( 0 < r2 & r2 < 1 ) and A25: g2 . r2 = ((p1 `1) + (p2 `1)) / 2 by A18, A22, A14, Th9; A26: [.0,1.] = { r3 where r3 is Element of REAL : ( 0 <= r3 & r3 <= 1 ) } by RCOMP_1:def_1; then A27: r2 in the carrier of I[01] by A24, BORSUK_1:40; dom f2 = the carrier of I[01] by FUNCT_2:def_1; then A28: f2 . r2 in rng f2 by A27, FUNCT_1:def_3; then A29: f2 . r2 in P by A9, A20, XBOOLE_0:def_3; f2 . r2 in P2 by A28, A20; then reconsider p4 = f2 . r2 as Point of (TOP-REAL 2) ; A30: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5; consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that A31: f1 is being_homeomorphism and A32: f1 . 0 = p1 and A33: f1 . 1 = p2 by A7, TOPREAL1:def_1; f1 is continuous by A31, TOPS_2:def_5; then consider g1 being Function of I[01],R^1 such that A34: g1 is continuous and A35: for r being Element of REAL for q1 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q1 = f1 . r holds q1 `1 = g1 . r by Th12; A36: p2 `1 = g1 . 1 by A33, A35, A21; p1 `1 = g1 . 0 by A32, A35, A23; then consider r1 being Element of REAL such that A37: ( 0 < r1 & r1 < 1 ) and A38: g1 . r1 = ((p1 `1) + (p2 `1)) / 2 by A34, A36, A14, Th9; A39: r1 in the carrier of I[01] by A37, A26, BORSUK_1:40; then r1 in dom f1 by FUNCT_2:def_1; then A40: f1 . r1 in rng f1 by FUNCT_1:def_3; then f1 . r1 in P1 by A30; then reconsider p3 = f1 . r1 as Point of (TOP-REAL 2) ; f1 . r1 in P by A9, A40, A30, XBOOLE_0:def_3; then A41: p3 `2 = r0 by A3 .= p4 `2 by A3, A29 ; p3 `1 = ((p1 `1) + (p2 `1)) / 2 by A35, A38, A39 .= p4 `1 by A19, A25, A27 ; then f1 . r1 = f2 . r2 by A41, TOPREAL3:6; then A42: f1 . r1 in P1 /\ P2 by A40, A30, A28, A20, XBOOLE_0:def_4; now__::_thesis:_(_(_f1_._r1_=_p1_&_contradiction_)_or_(_f1_._r1_=_p2_&_contradiction_)_) percases ( f1 . r1 = p1 or f1 . r1 = p2 ) by A10, A42, TARSKI:def_2; caseA43: f1 . r1 = p1 ; ::_thesis: contradiction A44: (((1 / 2) * p1) + ((1 / 2) * p2)) `2 = (((1 / 2) * p1) `2) + (((1 / 2) * p2) `2) by TOPREAL3:2 .= ((1 / 2) * (p1 `2)) + (((1 / 2) * p2) `2) by TOPREAL3:4 .= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4 .= r0 ; p1 `1 = ((2 ") * (p1 `1)) + ((p2 `1) / 2) by A35, A38, A39, A43 .= (((2 ") * p1) `1) + ((2 ") * (p2 `1)) by TOPREAL3:4 .= (((2 ") * p1) `1) + (((2 ") * p2) `1) by TOPREAL3:4 .= (((1 / 2) * p1) + ((1 / 2) * p2)) `1 by TOPREAL3:2 ; then p1 = ((1 / 2) * p1) + ((1 / 2) * p2) by A11, A44, TOPREAL3:6; then (1 * p1) - ((1 / 2) * p1) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1) by EUCLID:29; then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1)) by EUCLID:45; then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (0. (TOP-REAL 2)) by EUCLID:42; then (1 * p1) - ((1 / 2) * p1) = (1 / 2) * p2 by EUCLID:27; then (1 - (1 / 2)) * p1 = (1 / 2) * p2 by EUCLID:50; hence contradiction by A4, EUCLID:34; ::_thesis: verum end; caseA45: f1 . r1 = p2 ; ::_thesis: contradiction A46: (((1 / 2) * p1) + ((1 / 2) * p2)) `2 = (((1 / 2) * p1) `2) + (((1 / 2) * p2) `2) by TOPREAL3:2 .= ((1 / 2) * (p1 `2)) + (((1 / 2) * p2) `2) by TOPREAL3:4 .= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4 .= r0 ; p2 `1 = ((2 ") * (p1 `1)) + ((p2 `1) / 2) by A35, A38, A39, A45 .= (((2 ") * p1) `1) + ((2 ") * (p2 `1)) by TOPREAL3:4 .= (((2 ") * p1) `1) + (((2 ") * p2) `1) by TOPREAL3:4 .= (((1 / 2) * p1) + ((1 / 2) * p2)) `1 by TOPREAL3:2 ; then p2 = ((1 / 2) * p1) + ((1 / 2) * p2) by A12, A46, TOPREAL3:6; then (1 * p2) - ((1 / 2) * p2) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2) by EUCLID:29; then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2)) by EUCLID:45; then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (0. (TOP-REAL 2)) by EUCLID:42; then (1 * p2) - ((1 / 2) * p2) = (1 / 2) * p1 by EUCLID:27; then (1 - (1 / 2)) * p2 = (1 / 2) * p1 by EUCLID:50; hence contradiction by A4, EUCLID:34; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `2 = r ) ; ::_thesis: verum end; theorem Th15: :: TOPREAL5:15 for P being non empty Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `1 = r ) proof let P be non empty Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `1 = r ) ) assume A1: P is being_simple_closed_curve ; ::_thesis: for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `1 = r ) now__::_thesis:_for_r0_being_real_number_ex_p_being_Point_of_(TOP-REAL_2)_st_ (_p_in_P_&_not_p_`1_=_r0_) A2: [.0,1.] = ].0,1.[ \/ {0,1} by XXREAL_1:128; given r0 being real number such that A3: for p being Point of (TOP-REAL 2) st p in P holds p `1 = r0 ; ::_thesis: contradiction consider p1, p2 being Point of (TOP-REAL 2), P1, P2 being non empty Subset of (TOP-REAL 2) such that A4: p1 <> p2 and A5: p1 in P and A6: p2 in P and A7: P1 is_an_arc_of p1,p2 and A8: P2 is_an_arc_of p1,p2 and A9: P = P1 \/ P2 and A10: P1 /\ P2 = {p1,p2} by A1, TOPREAL2:6; A11: p1 `1 = r0 by A3, A5; A12: p2 `1 = r0 by A3, A6; then A13: p1 `1 = p2 `1 by A3, A5; A14: now__::_thesis:_not_p1_`2_=_p2_`2 assume p1 `2 = p2 `2 ; ::_thesis: contradiction then p1 = |[(p2 `1),(p2 `2)]| by A13, EUCLID:53; hence contradiction by A4, EUCLID:53; ::_thesis: verum end; consider f2 being Function of I[01],((TOP-REAL 2) | P2) such that A15: f2 is being_homeomorphism and A16: f2 . 0 = p1 and A17: f2 . 1 = p2 by A8, TOPREAL1:def_1; f2 is continuous by A15, TOPS_2:def_5; then consider g2 being Function of I[01],R^1 such that A18: g2 is continuous and A19: for r being Element of REAL for q2 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q2 = f2 . r holds q2 `2 = g2 . r by Th13; A20: [#] ((TOP-REAL 2) | P2) = P2 by PRE_TOPC:def_5; 1 in {0,1} by TARSKI:def_2; then A21: 1 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3; then A22: p2 `2 = g2 . 1 by A17, A19; 0 in {0,1} by TARSKI:def_2; then A23: 0 in the carrier of I[01] by A2, BORSUK_1:40, XBOOLE_0:def_3; then p1 `2 = g2 . 0 by A16, A19; then consider r2 being Element of REAL such that A24: ( 0 < r2 & r2 < 1 ) and A25: g2 . r2 = ((p1 `2) + (p2 `2)) / 2 by A18, A22, A14, Th9; A26: [.0,1.] = { r3 where r3 is Element of REAL : ( 0 <= r3 & r3 <= 1 ) } by RCOMP_1:def_1; then A27: r2 in the carrier of I[01] by A24, BORSUK_1:40; dom f2 = the carrier of I[01] by FUNCT_2:def_1; then A28: f2 . r2 in rng f2 by A27, FUNCT_1:def_3; then A29: f2 . r2 in P by A9, A20, XBOOLE_0:def_3; f2 . r2 in P2 by A28, A20; then reconsider p4 = f2 . r2 as Point of (TOP-REAL 2) ; A30: [#] ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:def_5; consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that A31: f1 is being_homeomorphism and A32: f1 . 0 = p1 and A33: f1 . 1 = p2 by A7, TOPREAL1:def_1; f1 is continuous by A31, TOPS_2:def_5; then consider g1 being Function of I[01],R^1 such that A34: g1 is continuous and A35: for r being Element of REAL for q1 being Point of (TOP-REAL 2) st r in the carrier of I[01] & q1 = f1 . r holds q1 `2 = g1 . r by Th13; A36: p2 `2 = g1 . 1 by A33, A35, A21; p1 `2 = g1 . 0 by A32, A35, A23; then consider r1 being Element of REAL such that A37: ( 0 < r1 & r1 < 1 ) and A38: g1 . r1 = ((p1 `2) + (p2 `2)) / 2 by A34, A36, A14, Th9; A39: r1 in the carrier of I[01] by A37, A26, BORSUK_1:40; then r1 in dom f1 by FUNCT_2:def_1; then A40: f1 . r1 in rng f1 by FUNCT_1:def_3; then f1 . r1 in P1 by A30; then reconsider p3 = f1 . r1 as Point of (TOP-REAL 2) ; f1 . r1 in P by A9, A40, A30, XBOOLE_0:def_3; then A41: p3 `1 = r0 by A3 .= p4 `1 by A3, A29 ; p3 `2 = ((p1 `2) + (p2 `2)) / 2 by A35, A38, A39 .= p4 `2 by A19, A25, A27 ; then f1 . r1 = f2 . r2 by A41, TOPREAL3:6; then A42: f1 . r1 in P1 /\ P2 by A40, A30, A28, A20, XBOOLE_0:def_4; now__::_thesis:_(_(_f1_._r1_=_p1_&_contradiction_)_or_(_f1_._r1_=_p2_&_contradiction_)_) percases ( f1 . r1 = p1 or f1 . r1 = p2 ) by A10, A42, TARSKI:def_2; caseA43: f1 . r1 = p1 ; ::_thesis: contradiction A44: (((1 / 2) * p1) + ((1 / 2) * p2)) `1 = (((1 / 2) * p1) `1) + (((1 / 2) * p2) `1) by TOPREAL3:2 .= ((1 / 2) * (p1 `1)) + (((1 / 2) * p2) `1) by TOPREAL3:4 .= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4 .= r0 ; p1 `2 = ((2 ") * (p1 `2)) + ((p2 `2) / 2) by A35, A38, A39, A43 .= (((2 ") * p1) `2) + ((2 ") * (p2 `2)) by TOPREAL3:4 .= (((2 ") * p1) `2) + (((2 ") * p2) `2) by TOPREAL3:4 .= (((1 / 2) * p1) + ((1 / 2) * p2)) `2 by TOPREAL3:2 ; then p1 = ((1 / 2) * p1) + ((1 / 2) * p2) by A11, A44, TOPREAL3:6; then (1 * p1) - ((1 / 2) * p1) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p1) by EUCLID:29; then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (((1 / 2) * p1) - ((1 / 2) * p1)) by EUCLID:45; then (1 * p1) - ((1 / 2) * p1) = ((1 / 2) * p2) + (0. (TOP-REAL 2)) by EUCLID:42; then (1 * p1) - ((1 / 2) * p1) = (1 / 2) * p2 by EUCLID:27; then (1 - (1 / 2)) * p1 = (1 / 2) * p2 by EUCLID:50; hence contradiction by A4, EUCLID:34; ::_thesis: verum end; caseA45: f1 . r1 = p2 ; ::_thesis: contradiction A46: (((1 / 2) * p1) + ((1 / 2) * p2)) `1 = (((1 / 2) * p1) `1) + (((1 / 2) * p2) `1) by TOPREAL3:2 .= ((1 / 2) * (p1 `1)) + (((1 / 2) * p2) `1) by TOPREAL3:4 .= ((1 / 2) * r0) + ((1 / 2) * r0) by A11, A12, TOPREAL3:4 .= r0 ; p2 `2 = ((2 ") * (p1 `2)) + ((p2 `2) / 2) by A35, A38, A39, A45 .= (((2 ") * p1) `2) + ((2 ") * (p2 `2)) by TOPREAL3:4 .= (((2 ") * p1) `2) + (((2 ") * p2) `2) by TOPREAL3:4 .= (((1 / 2) * p1) + ((1 / 2) * p2)) `2 by TOPREAL3:2 ; then p2 = ((1 / 2) * p1) + ((1 / 2) * p2) by A12, A46, TOPREAL3:6; then (1 * p2) - ((1 / 2) * p2) = (((1 / 2) * p1) + ((1 / 2) * p2)) - ((1 / 2) * p2) by EUCLID:29; then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (((1 / 2) * p2) - ((1 / 2) * p2)) by EUCLID:45; then (1 * p2) - ((1 / 2) * p2) = ((1 / 2) * p1) + (0. (TOP-REAL 2)) by EUCLID:42; then (1 * p2) - ((1 / 2) * p2) = (1 / 2) * p1 by EUCLID:27; then (1 - (1 / 2)) * p2 = (1 / 2) * p1 by EUCLID:50; hence contradiction by A4, EUCLID:34; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence for r being Element of REAL ex p being Point of (TOP-REAL 2) st ( p in P & not p `1 = r ) ; ::_thesis: verum end; theorem Th16: :: TOPREAL5:16 for C being non empty compact Subset of (TOP-REAL 2) st C is being_simple_closed_curve holds N-bound C > S-bound C proof let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is being_simple_closed_curve implies N-bound C > S-bound C ) assume A1: C is being_simple_closed_curve ; ::_thesis: N-bound C > S-bound C now__::_thesis:_not_N-bound_C_<=_S-bound_C assume A2: N-bound C <= S-bound C ; ::_thesis: contradiction for p being Point of (TOP-REAL 2) st p in C holds p `2 = S-bound C proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies p `2 = S-bound C ) assume p in C ; ::_thesis: p `2 = S-bound C then A3: ( S-bound C <= p `2 & p `2 <= N-bound C ) by PSCOMP_1:24; then S-bound C <= N-bound C by XXREAL_0:2; then S-bound C = N-bound C by A2, XXREAL_0:1; hence p `2 = S-bound C by A3, XXREAL_0:1; ::_thesis: verum end; hence contradiction by A1, Th14; ::_thesis: verum end; hence N-bound C > S-bound C ; ::_thesis: verum end; theorem Th17: :: TOPREAL5:17 for C being non empty compact Subset of (TOP-REAL 2) st C is being_simple_closed_curve holds E-bound C > W-bound C proof let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( C is being_simple_closed_curve implies E-bound C > W-bound C ) assume A1: C is being_simple_closed_curve ; ::_thesis: E-bound C > W-bound C now__::_thesis:_not_E-bound_C_<=_W-bound_C assume A2: E-bound C <= W-bound C ; ::_thesis: contradiction for p being Point of (TOP-REAL 2) st p in C holds p `1 = W-bound C proof let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies p `1 = W-bound C ) assume p in C ; ::_thesis: p `1 = W-bound C then A3: ( W-bound C <= p `1 & p `1 <= E-bound C ) by PSCOMP_1:24; then W-bound C <= E-bound C by XXREAL_0:2; then W-bound C = E-bound C by A2, XXREAL_0:1; hence p `1 = W-bound C by A3, XXREAL_0:1; ::_thesis: verum end; hence contradiction by A1, Th15; ::_thesis: verum end; hence E-bound C > W-bound C ; ::_thesis: verum end; theorem :: TOPREAL5:18 for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds S-min P <> N-max P proof let P be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies S-min P <> N-max P ) assume A1: P is being_simple_closed_curve ; ::_thesis: S-min P <> N-max P now__::_thesis:_not_S-min_P_=_N-max_P A2: ( |[(lower_bound (proj1 | (S-most P))),(S-bound P)]| = S-min P & |[(upper_bound (proj1 | (N-most P))),(N-bound P)]| = N-max P ) by PSCOMP_1:def_22, PSCOMP_1:def_26; assume S-min P = N-max P ; ::_thesis: contradiction then S-bound P = N-bound P by A2, SPPOL_2:1; hence contradiction by A1, Th16; ::_thesis: verum end; hence S-min P <> N-max P ; ::_thesis: verum end; theorem :: TOPREAL5:19 for P being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds W-min P <> E-max P proof let P be non empty compact Subset of (TOP-REAL 2); ::_thesis: ( P is being_simple_closed_curve implies W-min P <> E-max P ) assume A1: P is being_simple_closed_curve ; ::_thesis: W-min P <> E-max P now__::_thesis:_not_W-min_P_=_E-max_P A2: ( |[(W-bound P),(lower_bound (proj2 | (W-most P)))]| = W-min P & |[(E-bound P),(upper_bound (proj2 | (E-most P)))]| = E-max P ) by PSCOMP_1:def_19, PSCOMP_1:def_23; assume W-min P = E-max P ; ::_thesis: contradiction then W-bound P = E-bound P by A2, SPPOL_2:1; hence contradiction by A1, Th17; ::_thesis: verum end; hence W-min P <> E-max P ; ::_thesis: verum end; registration cluster being_simple_closed_curve -> non horizontal non vertical for Element of K6( the carrier of (TOP-REAL 2)); coherence for b1 being Simple_closed_curve holds ( not b1 is vertical & not b1 is horizontal ) proof let S be Simple_closed_curve; ::_thesis: ( not S is vertical & not S is horizontal ) consider p1 being set such that A1: p1 in S by XBOOLE_0:def_1; reconsider p1 = p1 as Point of (TOP-REAL 2) by A1; ex p2 being Point of (TOP-REAL 2) st ( p2 in S & p2 `1 <> p1 `1 ) by Th15; hence not S is vertical by A1, SPPOL_1:def_3; ::_thesis: not S is horizontal ex p2 being Point of (TOP-REAL 2) st ( p2 in S & p2 `2 <> p1 `2 ) by Th14; hence not S is horizontal by A1, SPPOL_1:def_2; ::_thesis: verum end; end;