:: JORDAN17 semantic presentation begin theorem Th1: :: JORDAN17:1 for n being Element of NAT for a, p1, p2 being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds ex f being Function of I[01],((TOP-REAL n) | P) ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) proof let n be Element of NAT ; ::_thesis: for a, p1, p2 being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds ex f being Function of I[01],((TOP-REAL n) | P) ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) let a, p1, p2 be Point of (TOP-REAL n); ::_thesis: for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds ex f being Function of I[01],((TOP-REAL n) | P) ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) let P be Subset of (TOP-REAL n); ::_thesis: ( a in P & P is_an_arc_of p1,p2 implies ex f being Function of I[01],((TOP-REAL n) | P) ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) ) assume A1: a in P ; ::_thesis: ( not P is_an_arc_of p1,p2 or ex f being Function of I[01],((TOP-REAL n) | P) ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) ) given f being Function of I[01],((TOP-REAL n) | P) such that A2: f is being_homeomorphism and A3: ( f . 0 = p1 & f . 1 = p2 ) ; :: according to TOPREAL1:def_1 ::_thesis: ex f being Function of I[01],((TOP-REAL n) | P) ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) rng f = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def_5 .= the carrier of ((TOP-REAL n) | P) .= P by PRE_TOPC:8 ; then consider r being set such that A4: r in dom f and A5: a = f . r by A1, FUNCT_1:def_3; A6: dom f = [#] I[01] by A2, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then reconsider r = r as Real by A4; take f ; ::_thesis: ex r being Real st ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) take r ; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= r & r <= 1 & f . r = a ) thus ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A2, A3; ::_thesis: ( 0 <= r & r <= 1 & f . r = a ) thus ( 0 <= r & r <= 1 ) by A4, A6, XXREAL_1:1; ::_thesis: f . r = a thus f . r = a by A5; ::_thesis: verum end; theorem :: JORDAN17:2 for P being Simple_closed_curve holds LE W-min P, E-max P,P proof let P be Simple_closed_curve; ::_thesis: LE W-min P, E-max P,P A1: E-max P <> W-min P by TOPREAL5:19; ( W-min P in Upper_Arc P & E-max P in Lower_Arc P ) by JORDAN7:1; hence LE W-min P, E-max P,P by A1, JORDAN6:def_10; ::_thesis: verum end; theorem :: JORDAN17:3 for P being Simple_closed_curve for a being Point of (TOP-REAL 2) st LE a, E-max P,P holds a in Upper_Arc P proof let P be Simple_closed_curve; ::_thesis: for a being Point of (TOP-REAL 2) st LE a, E-max P,P holds a in Upper_Arc P let a be Point of (TOP-REAL 2); ::_thesis: ( LE a, E-max P,P implies a in Upper_Arc P ) assume A1: LE a, E-max P,P ; ::_thesis: a in Upper_Arc P percases ( ( a in Upper_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P ) or ( a in Upper_Arc P & E-max P in Upper_Arc P & LE a, E-max P, Upper_Arc P, W-min P, E-max P ) or ( a in Lower_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P & LE a, E-max P, Lower_Arc P, E-max P, W-min P ) ) by A1, JORDAN6:def_10; suppose ( ( a in Upper_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P ) or ( a in Upper_Arc P & E-max P in Upper_Arc P & LE a, E-max P, Upper_Arc P, W-min P, E-max P ) ) ; ::_thesis: a in Upper_Arc P hence a in Upper_Arc P ; ::_thesis: verum end; supposethat A2: a in Lower_Arc P and ( E-max P in Lower_Arc P & not E-max P = W-min P ) and A3: LE a, E-max P, Lower_Arc P, E-max P, W-min P ; ::_thesis: a in Upper_Arc P Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def_9; then consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)), r being Real such that A4: f is being_homeomorphism and A5: f . 0 = E-max P and A6: f . 1 = W-min P and A7: 0 <= r and A8: r <= 1 and A9: f . r = a by A2, Th1; thus a in Upper_Arc P ::_thesis: verum proof percases ( r = 0 or r <> 0 ) ; suppose r = 0 ; ::_thesis: a in Upper_Arc P hence a in Upper_Arc P by A5, A9, JORDAN7:1; ::_thesis: verum end; suppose r <> 0 ; ::_thesis: a in Upper_Arc P then r > 0 by A7, XXREAL_0:1; hence a in Upper_Arc P by A3, A4, A5, A6, A8, A9, JORDAN5C:def_3; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:4 for P being Simple_closed_curve for a being Point of (TOP-REAL 2) st LE E-max P,a,P holds a in Lower_Arc P proof let P be Simple_closed_curve; ::_thesis: for a being Point of (TOP-REAL 2) st LE E-max P,a,P holds a in Lower_Arc P let a be Point of (TOP-REAL 2); ::_thesis: ( LE E-max P,a,P implies a in Lower_Arc P ) assume A1: LE E-max P,a,P ; ::_thesis: a in Lower_Arc P percases ( ( E-max P in Upper_Arc P & a in Lower_Arc P & not a = W-min P ) or ( E-max P in Lower_Arc P & a in Lower_Arc P & not a = W-min P & LE E-max P,a, Lower_Arc P, E-max P, W-min P ) or ( E-max P in Upper_Arc P & a in Upper_Arc P & LE E-max P,a, Upper_Arc P, W-min P, E-max P ) ) by A1, JORDAN6:def_10; suppose ( ( E-max P in Upper_Arc P & a in Lower_Arc P & not a = W-min P ) or ( E-max P in Lower_Arc P & a in Lower_Arc P & not a = W-min P & LE E-max P,a, Lower_Arc P, E-max P, W-min P ) ) ; ::_thesis: a in Lower_Arc P hence a in Lower_Arc P ; ::_thesis: verum end; supposethat E-max P in Upper_Arc P and A2: a in Upper_Arc P and A3: LE E-max P,a, Upper_Arc P, W-min P, E-max P ; ::_thesis: a in Lower_Arc P Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def_8; then consider f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)), r being Real such that A4: ( f is being_homeomorphism & f . 0 = W-min P ) and A5: f . 1 = E-max P and A6: 0 <= r and A7: r <= 1 and A8: f . r = a by A2, Th1; thus a in Lower_Arc P ::_thesis: verum proof percases ( r = 1 or r <> 1 ) ; suppose r = 1 ; ::_thesis: a in Lower_Arc P hence a in Lower_Arc P by A5, A8, JORDAN7:1; ::_thesis: verum end; suppose r <> 1 ; ::_thesis: a in Lower_Arc P then r < 1 by A7, XXREAL_0:1; hence a in Lower_Arc P by A3, A4, A5, A6, A8, JORDAN5C:def_3; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:5 for P being Simple_closed_curve for a being Point of (TOP-REAL 2) st LE a, W-min P,P holds a in Lower_Arc P proof let P be Simple_closed_curve; ::_thesis: for a being Point of (TOP-REAL 2) st LE a, W-min P,P holds a in Lower_Arc P let a be Point of (TOP-REAL 2); ::_thesis: ( LE a, W-min P,P implies a in Lower_Arc P ) assume A1: LE a, W-min P,P ; ::_thesis: a in Lower_Arc P percases ( ( a in Upper_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P ) or ( a in Lower_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P & LE a, W-min P, Lower_Arc P, E-max P, W-min P ) or ( a in Upper_Arc P & W-min P in Upper_Arc P & LE a, W-min P, Upper_Arc P, W-min P, E-max P ) ) by A1, JORDAN6:def_10; suppose ( ( a in Upper_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P ) or ( a in Lower_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P & LE a, W-min P, Lower_Arc P, E-max P, W-min P ) ) ; ::_thesis: a in Lower_Arc P hence a in Lower_Arc P ; ::_thesis: verum end; supposethat A2: a in Upper_Arc P and W-min P in Upper_Arc P and A3: LE a, W-min P, Upper_Arc P, W-min P, E-max P ; ::_thesis: a in Lower_Arc P Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def_8; then consider f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)), r being Real such that A4: f is being_homeomorphism and A5: f . 0 = W-min P and A6: f . 1 = E-max P and A7: 0 <= r and A8: r <= 1 and A9: f . r = a by A2, Th1; thus a in Lower_Arc P ::_thesis: verum proof percases ( r = 0 or r <> 0 ) ; suppose r = 0 ; ::_thesis: a in Lower_Arc P hence a in Lower_Arc P by A5, A9, JORDAN7:1; ::_thesis: verum end; suppose r <> 0 ; ::_thesis: a in Lower_Arc P then r > 0 by A7, XXREAL_0:1; hence a in Lower_Arc P by A3, A4, A5, A6, A8, A9, JORDAN5C:def_3; ::_thesis: verum end; end; end; end; end; end; theorem Th6: :: JORDAN17:6 for a, b, c, d being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) st a <> b & P is_an_arc_of c,d & LE a,b,P,c,d holds ex e being Point of (TOP-REAL 2) st ( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d ) proof let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: for P being Subset of (TOP-REAL 2) st a <> b & P is_an_arc_of c,d & LE a,b,P,c,d holds ex e being Point of (TOP-REAL 2) st ( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d ) let P be Subset of (TOP-REAL 2); ::_thesis: ( a <> b & P is_an_arc_of c,d & LE a,b,P,c,d implies ex e being Point of (TOP-REAL 2) st ( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d ) ) assume that A1: a <> b and A2: P is_an_arc_of c,d and A3: LE a,b,P,c,d ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d ) b in P by A3, JORDAN5C:def_3; then consider f being Function of I[01],((TOP-REAL 2) | P), rb being Real such that A4: f is being_homeomorphism and A5: ( f . 0 = c & f . 1 = d ) and A6: 0 <= rb and A7: rb <= 1 and A8: f . rb = b by A2, Th1; A9: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5 .= the carrier of ((TOP-REAL 2) | P) .= P by PRE_TOPC:8 ; a in P by A3, JORDAN5C:def_3; then consider ra being set such that A10: ra in dom f and A11: a = f . ra by A9, FUNCT_1:def_3; A12: dom f = [#] I[01] by A4, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; then reconsider ra = ra as Real by A10; A13: 0 <= ra by A10, A12, XXREAL_1:1; A14: ra <= 1 by A10, A12, XXREAL_1:1; then ra <= rb by A3, A4, A5, A6, A7, A8, A11, A13, JORDAN5C:def_3; then ra < rb by A1, A8, A11, XXREAL_0:1; then consider re being real number such that A15: ra < re and A16: re < rb by XREAL_1:5; set e = f . re; A17: re <= 1 by A7, A16, XXREAL_0:2; A18: 0 <= re by A13, A15, XXREAL_0:2; then A19: re in dom f by A12, A17, XXREAL_1:1; then f . re in rng f by FUNCT_1:def_3; then reconsider e = f . re as Point of (TOP-REAL 2) by A9; take e ; ::_thesis: ( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d ) now__::_thesis:_(_not_a_=_e_&_not_b_=_e_) assume A20: ( a = e or b = e ) ; ::_thesis: contradiction ( f is one-to-one & rb in dom f ) by A4, A6, A7, A12, TOPS_2:def_5, XXREAL_1:1; hence contradiction by A8, A10, A11, A15, A16, A19, A20, FUNCT_1:def_4; ::_thesis: verum end; hence ( a <> e & b <> e ) ; ::_thesis: ( LE a,e,P,c,d & LE e,b,P,c,d ) re is Real by XREAL_0:def_1; hence ( LE a,e,P,c,d & LE e,b,P,c,d ) by A2, A4, A5, A6, A7, A8, A11, A13, A14, A15, A16, A18, A17, JORDAN5C:8; ::_thesis: verum end; theorem Th7: :: JORDAN17:7 for P being Simple_closed_curve for a being Point of (TOP-REAL 2) st a in P holds ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) proof let P be Simple_closed_curve; ::_thesis: for a being Point of (TOP-REAL 2) st a in P holds ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) let a be Point of (TOP-REAL 2); ::_thesis: ( a in P implies ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) ) assume A1: a in P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) A2: E-max P <> W-min P by TOPREAL5:19; A3: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def_9; percases ( a = W-min P or a <> W-min P ) ; supposeA4: a = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) take E-max P ; ::_thesis: ( a <> E-max P & LE a, E-max P,P ) thus ( a <> E-max P & LE a, E-max P,P ) by A4, JORDAN7:3, SPRECT_1:14, TOPREAL5:19; ::_thesis: verum end; supposeA5: a <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) thus ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) ::_thesis: verum proof percases ( a in Upper_Arc P or not a in Upper_Arc P ) ; supposeA6: a in Upper_Arc P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) thus ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) ::_thesis: verum proof percases ( a = E-max P or a <> E-max P ) ; supposeA7: a = E-max P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) consider e being Point of (TOP-REAL 2) such that A8: ( e in Lower_Arc P & e <> E-max P & e <> W-min P ) by A3, JORDAN6:42; take e ; ::_thesis: ( a <> e & LE a,e,P ) thus ( a <> e & LE a,e,P ) by A6, A7, A8, JORDAN6:def_10; ::_thesis: verum end; supposeA9: a <> E-max P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) take E-max P ; ::_thesis: ( a <> E-max P & LE a, E-max P,P ) E-max P in Lower_Arc P by JORDAN7:1; hence ( a <> E-max P & LE a, E-max P,P ) by A2, A6, A9, JORDAN6:def_10; ::_thesis: verum end; end; end; end; supposeA10: not a in Upper_Arc P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( a <> e & LE a,e,P ) (Upper_Arc P) \/ (Lower_Arc P) = P by JORDAN6:def_9; then A11: a in Lower_Arc P by A1, A10, XBOOLE_0:def_3; then consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)), r being Real such that A12: f is being_homeomorphism and A13: f . 0 = E-max P and A14: f . 1 = W-min P and A15: 0 <= r and A16: r <= 1 and A17: f . r = a by A3, Th1; A18: f is one-to-one by A12, TOPS_2:def_5; r < 1 by A5, A14, A16, A17, XXREAL_0:1; then consider s being real number such that A19: r < s and A20: s < 1 by XREAL_1:5; A21: dom f = [#] I[01] by A12, TOPS_2:def_5 .= [.0,1.] by BORSUK_1:40 ; A22: rng f = [#] ((TOP-REAL 2) | (Lower_Arc P)) by A12, TOPS_2:def_5 .= the carrier of ((TOP-REAL 2) | (Lower_Arc P)) .= Lower_Arc P by PRE_TOPC:8 ; A23: 0 <= s by A15, A19, XXREAL_0:2; then A24: s in dom f by A21, A20, XXREAL_1:1; then A25: f . s in rng f by FUNCT_1:def_3; then reconsider e = f . s as Point of (TOP-REAL 2) by A22; 1 in dom f by A21, XXREAL_1:1; then A26: e <> W-min P by A14, A18, A20, A24, FUNCT_1:def_4; take e ; ::_thesis: ( a <> e & LE a,e,P ) r in dom f by A15, A16, A21, XXREAL_1:1; hence a <> e by A17, A18, A19, A24, FUNCT_1:def_4; ::_thesis: LE a,e,P s is Real by XREAL_0:def_1; then LE a,e, Lower_Arc P, E-max P, W-min P by A3, A12, A13, A14, A15, A16, A17, A19, A20, A23, JORDAN5C:8; hence LE a,e,P by A11, A22, A25, A26, JORDAN6:def_10; ::_thesis: verum end; end; end; end; end; end; theorem Th8: :: JORDAN17:8 for P being Simple_closed_curve for a, b being Point of (TOP-REAL 2) st a <> b & LE a,b,P holds ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) proof let P be Simple_closed_curve; ::_thesis: for a, b being Point of (TOP-REAL 2) st a <> b & LE a,b,P holds ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) let a, b be Point of (TOP-REAL 2); ::_thesis: ( a <> b & LE a,b,P implies ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) ) assume that A1: a <> b and A2: LE a,b,P ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) A3: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def_8; A4: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def_9; percases ( ( a in Upper_Arc P & b in Lower_Arc P & not b = W-min P ) or ( a in Upper_Arc P & b in Upper_Arc P & LE a,b, Upper_Arc P, W-min P, E-max P ) or ( a in Lower_Arc P & b in Lower_Arc P & not b = W-min P & LE a,b, Lower_Arc P, E-max P, W-min P ) ) by A2, JORDAN6:def_10; supposethat A5: a in Upper_Arc P and A6: b in Lower_Arc P and A7: not b = W-min P ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) A8: E-max P in Lower_Arc P by JORDAN7:1; A9: ( E-max P in Upper_Arc P & E-max P <> W-min P ) by JORDAN7:1, TOPREAL5:19; thus ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) ::_thesis: verum proof percases ( ( a <> E-max P & b <> E-max P ) or a = E-max P or b = E-max P ) ; supposeA10: ( a <> E-max P & b <> E-max P ) ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) take e = E-max P; ::_thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) thus ( a <> e & b <> e ) by A10; ::_thesis: ( LE a,e,P & LE e,b,P ) thus ( LE a,e,P & LE e,b,P ) by A5, A6, A7, A8, A9, JORDAN6:def_10; ::_thesis: verum end; supposeA11: a = E-max P ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) then LE a,b, Lower_Arc P, E-max P, W-min P by A4, A6, JORDAN5C:10; then consider e being Point of (TOP-REAL 2) such that A12: ( a <> e & b <> e ) and A13: ( LE a,e, Lower_Arc P, E-max P, W-min P & LE e,b, Lower_Arc P, E-max P, W-min P ) by A1, A4, Th6; take e ; ::_thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) thus ( e <> a & e <> b ) by A12; ::_thesis: ( LE a,e,P & LE e,b,P ) ( e in Lower_Arc P & e <> W-min P ) by A4, A7, A13, JORDAN5C:def_3, JORDAN6:55; hence ( LE a,e,P & LE e,b,P ) by A6, A7, A8, A11, A13, JORDAN6:def_10; ::_thesis: verum end; supposeA14: b = E-max P ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) then LE a,b, Upper_Arc P, W-min P, E-max P by A3, A5, JORDAN5C:10; then consider e being Point of (TOP-REAL 2) such that A15: ( a <> e & b <> e ) and A16: LE a,e, Upper_Arc P, W-min P, E-max P and LE e,b, Upper_Arc P, W-min P, E-max P by A1, A3, Th6; take e ; ::_thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) thus ( e <> a & e <> b ) by A15; ::_thesis: ( LE a,e,P & LE e,b,P ) e in Upper_Arc P by A16, JORDAN5C:def_3; hence ( LE a,e,P & LE e,b,P ) by A5, A7, A8, A14, A16, JORDAN6:def_10; ::_thesis: verum end; end; end; end; supposethat A17: ( a in Upper_Arc P & b in Upper_Arc P ) and A18: LE a,b, Upper_Arc P, W-min P, E-max P ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) consider e being Point of (TOP-REAL 2) such that A19: ( a <> e & b <> e ) and A20: LE a,e, Upper_Arc P, W-min P, E-max P and A21: LE e,b, Upper_Arc P, W-min P, E-max P by A1, A3, A18, Th6; take e ; ::_thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) thus ( e <> a & e <> b ) by A19; ::_thesis: ( LE a,e,P & LE e,b,P ) e in Upper_Arc P by A20, JORDAN5C:def_3; hence ( LE a,e,P & LE e,b,P ) by A17, A20, A21, JORDAN6:def_10; ::_thesis: verum end; supposethat A22: ( a in Lower_Arc P & b in Lower_Arc P ) and A23: not b = W-min P and A24: LE a,b, Lower_Arc P, E-max P, W-min P ; ::_thesis: ex c being Point of (TOP-REAL 2) st ( c <> a & c <> b & LE a,c,P & LE c,b,P ) consider e being Point of (TOP-REAL 2) such that A25: ( a <> e & b <> e ) and A26: LE a,e, Lower_Arc P, E-max P, W-min P and A27: LE e,b, Lower_Arc P, E-max P, W-min P by A1, A4, A24, Th6; take e ; ::_thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) thus ( e <> a & e <> b ) by A25; ::_thesis: ( LE a,e,P & LE e,b,P ) A28: e in Lower_Arc P by A26, JORDAN5C:def_3; e <> W-min P by A4, A23, A27, JORDAN6:55; hence ( LE a,e,P & LE e,b,P ) by A22, A23, A26, A27, A28, JORDAN6:def_10; ::_thesis: verum end; end; end; definition let P be Subset of (TOP-REAL 2); let a, b, c, d be Point of (TOP-REAL 2); preda,b,c,d are_in_this_order_on P means :Def1: :: JORDAN17:def 1 ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ); end; :: deftheorem Def1 defines are_in_this_order_on JORDAN17:def_1_:_ for P being Subset of (TOP-REAL 2) for a, b, c, d being Point of (TOP-REAL 2) holds ( a,b,c,d are_in_this_order_on P iff ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ); theorem :: JORDAN17:9 for P being Simple_closed_curve for a being Point of (TOP-REAL 2) st a in P holds a,a,a,a are_in_this_order_on P proof let P be Simple_closed_curve; ::_thesis: for a being Point of (TOP-REAL 2) st a in P holds a,a,a,a are_in_this_order_on P let a be Point of (TOP-REAL 2); ::_thesis: ( a in P implies a,a,a,a are_in_this_order_on P ) assume a in P ; ::_thesis: a,a,a,a are_in_this_order_on P then LE a,a,P by JORDAN6:56; hence a,a,a,a are_in_this_order_on P by Def1; ::_thesis: verum end; theorem :: JORDAN17:10 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds b,c,d,a are_in_this_order_on P proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds b,c,d,a are_in_this_order_on P let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a,b,c,d are_in_this_order_on P implies b,c,d,a are_in_this_order_on P ) assume ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: b,c,d,a are_in_this_order_on P hence ( ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) or ( LE a,b,P & LE b,c,P & LE c,d,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: verum end; theorem :: JORDAN17:11 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds c,d,a,b are_in_this_order_on P proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds c,d,a,b are_in_this_order_on P let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a,b,c,d are_in_this_order_on P implies c,d,a,b are_in_this_order_on P ) assume ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: c,d,a,b are_in_this_order_on P hence ( ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) or ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: verum end; theorem :: JORDAN17:12 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds d,a,b,c are_in_this_order_on P proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds d,a,b,c are_in_this_order_on P let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a,b,c,d are_in_this_order_on P implies d,a,b,c are_in_this_order_on P ) assume ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: d,a,b,c are_in_this_order_on P hence ( ( LE d,a,P & LE a,b,P & LE b,c,P ) or ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: verum end; theorem :: JORDAN17:13 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a <> b & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) ) assume that A1: a <> b and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposeA3: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) then consider e being Point of (TOP-REAL 2) such that A4: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, Th8; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) thus ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) by A3, A4, Def1; ::_thesis: verum end; supposethat A5: LE b,c,P and A6: LE c,d,P and A7: LE d,a,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) ::_thesis: verum proof A8: LE c,a,P by A6, A7, JORDAN6:58; percases ( b = W-min P or b <> W-min P ) ; supposeA9: b = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) a in P by A7, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A10: e <> a and A11: LE a,e,P by Th7; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) thus e <> a by A10; ::_thesis: ( e <> b & a,e,b,c are_in_this_order_on P ) thus e <> b by A1, A9, A11, JORDAN7:2; ::_thesis: a,e,b,c are_in_this_order_on P thus a,e,b,c are_in_this_order_on P by A5, A8, A11, Def1; ::_thesis: verum end; supposeA12: b <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) b in P by A5, JORDAN7:5; then A13: LE e,b,P by JORDAN7:3; now__::_thesis:_not_e_=_a LE b,d,P by A5, A6, JORDAN6:58; then A14: LE b,a,P by A7, JORDAN6:58; assume e = a ; ::_thesis: contradiction hence contradiction by A1, A13, A14, JORDAN6:57; ::_thesis: verum end; hence e <> a ; ::_thesis: ( e <> b & a,e,b,c are_in_this_order_on P ) thus e <> b by A12; ::_thesis: a,e,b,c are_in_this_order_on P thus a,e,b,c are_in_this_order_on P by A5, A8, A13, Def1; ::_thesis: verum end; end; end; end; supposethat A15: LE c,d,P and A16: ( LE d,a,P & LE a,b,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A17: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A16, Th8; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) LE c,a,P by A15, A16, JORDAN6:58; hence ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) by A17, Def1; ::_thesis: verum end; supposethat A18: ( LE d,a,P & LE a,b,P ) and A19: LE b,c,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A20: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A18, Th8; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) thus ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) by A19, A20, Def1; ::_thesis: verum end; end; end; theorem :: JORDAN17:14 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a <> b & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) ) assume that A1: a <> b and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposethat A3: LE a,b,P and A4: ( LE b,c,P & LE c,d,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A5: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A3, Th8; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) LE b,d,P by A4, JORDAN6:58; hence ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) by A5, Def1; ::_thesis: verum end; supposethat A6: LE b,c,P and A7: LE c,d,P and A8: LE d,a,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) ::_thesis: verum proof A9: LE b,d,P by A6, A7, JORDAN6:58; percases ( b = W-min P or b <> W-min P ) ; supposeA10: b = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) a in P by A8, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A11: e <> a and A12: LE a,e,P by Th7; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) thus e <> a by A11; ::_thesis: ( e <> b & a,e,b,d are_in_this_order_on P ) thus e <> b by A1, A10, A12, JORDAN7:2; ::_thesis: a,e,b,d are_in_this_order_on P thus a,e,b,d are_in_this_order_on P by A8, A9, A12, Def1; ::_thesis: verum end; supposeA13: b <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) b in P by A6, JORDAN7:5; then A14: LE e,b,P by JORDAN7:3; now__::_thesis:_not_e_=_a LE b,d,P by A6, A7, JORDAN6:58; then A15: LE b,a,P by A8, JORDAN6:58; assume e = a ; ::_thesis: contradiction hence contradiction by A1, A14, A15, JORDAN6:57; ::_thesis: verum end; hence e <> a ; ::_thesis: ( e <> b & a,e,b,d are_in_this_order_on P ) thus e <> b by A13; ::_thesis: a,e,b,d are_in_this_order_on P thus a,e,b,d are_in_this_order_on P by A8, A9, A14, Def1; ::_thesis: verum end; end; end; end; supposethat LE c,d,P and A16: LE d,a,P and A17: LE a,b,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A18: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A17, Th8; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) thus ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) by A16, A18, Def1; ::_thesis: verum end; supposethat A19: LE d,a,P and A20: LE a,b,P and LE b,c,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A21: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A20, Th8; take e ; ::_thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) thus ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) by A19, A21, Def1; ::_thesis: verum end; end; end; theorem :: JORDAN17:15 for P being Simple_closed_curve for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) let b, c, a, d be Point of (TOP-REAL 2); ::_thesis: ( b <> c & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) ) assume that A1: b <> c and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposeA3: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) then consider e being Point of (TOP-REAL 2) such that A4: ( e <> b & e <> c & LE b,e,P & LE e,c,P ) by A1, Th8; take e ; ::_thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) thus ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) by A3, A4, Def1; ::_thesis: verum end; supposethat A5: LE b,c,P and A6: ( LE c,d,P & LE d,a,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A7: ( e <> b & e <> c & LE b,e,P & LE e,c,P ) by A1, A5, Th8; take e ; ::_thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) LE c,a,P by A6, JORDAN6:58; hence ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) by A7, Def1; ::_thesis: verum end; supposethat A8: LE c,d,P and A9: LE d,a,P and A10: LE a,b,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) ::_thesis: verum proof A11: LE c,a,P by A8, A9, JORDAN6:58; percases ( c = W-min P or c <> W-min P ) ; supposeA12: c = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) b in P by A10, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A13: e <> b and A14: LE b,e,P by Th7; take e ; ::_thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) thus e <> b by A13; ::_thesis: ( e <> c & a,b,e,c are_in_this_order_on P ) thus e <> c by A1, A12, A14, JORDAN7:2; ::_thesis: a,b,e,c are_in_this_order_on P thus a,b,e,c are_in_this_order_on P by A10, A11, A14, Def1; ::_thesis: verum end; supposeA15: c <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) c in P by A8, JORDAN7:5; then A16: LE e,c,P by JORDAN7:3; now__::_thesis:_not_e_=_b LE c,a,P by A8, A9, JORDAN6:58; then A17: LE c,b,P by A10, JORDAN6:58; assume e = b ; ::_thesis: contradiction hence contradiction by A1, A16, A17, JORDAN6:57; ::_thesis: verum end; hence e <> b ; ::_thesis: ( e <> c & a,b,e,c are_in_this_order_on P ) thus e <> c by A15; ::_thesis: a,b,e,c are_in_this_order_on P thus a,b,e,c are_in_this_order_on P by A10, A11, A16, Def1; ::_thesis: verum end; end; end; end; supposethat LE d,a,P and A18: ( LE a,b,P & LE b,c,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A19: ( e <> b & e <> c & LE b,e,P & LE e,c,P ) by A1, A18, Th8; take e ; ::_thesis: ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) thus ( e <> b & e <> c & a,b,e,c are_in_this_order_on P ) by A18, A19, Def1; ::_thesis: verum end; end; end; theorem :: JORDAN17:16 for P being Simple_closed_curve for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for b, c, a, d being Point of (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) let b, c, a, d be Point of (TOP-REAL 2); ::_thesis: ( b <> c & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) ) assume that A1: b <> c and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposeA3: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) then consider e being Point of (TOP-REAL 2) such that A4: ( e <> b & e <> c & LE b,e,P & LE e,c,P ) by A1, Th8; take e ; ::_thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) thus ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) by A3, A4, Def1; ::_thesis: verum end; supposeA5: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) then consider e being Point of (TOP-REAL 2) such that A6: ( e <> b & e <> c & LE b,e,P & LE e,c,P ) by A1, Th8; take e ; ::_thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) thus ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) by A5, A6, Def1; ::_thesis: verum end; supposethat A7: LE c,d,P and A8: LE d,a,P and A9: LE a,b,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) ::_thesis: verum proof A10: LE d,b,P by A8, A9, JORDAN6:58; percases ( c = W-min P or c <> W-min P ) ; supposeA11: c = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) b in P by A9, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A12: e <> b and A13: LE b,e,P by Th7; take e ; ::_thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) thus e <> b by A12; ::_thesis: ( e <> c & b,e,c,d are_in_this_order_on P ) thus e <> c by A1, A11, A13, JORDAN7:2; ::_thesis: b,e,c,d are_in_this_order_on P thus b,e,c,d are_in_this_order_on P by A7, A10, A13, Def1; ::_thesis: verum end; supposeA14: c <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) c in P by A7, JORDAN7:5; then A15: LE e,c,P by JORDAN7:3; now__::_thesis:_not_e_=_b LE c,a,P by A7, A8, JORDAN6:58; then A16: LE c,b,P by A9, JORDAN6:58; assume e = b ; ::_thesis: contradiction hence contradiction by A1, A15, A16, JORDAN6:57; ::_thesis: verum end; hence e <> b ; ::_thesis: ( e <> c & b,e,c,d are_in_this_order_on P ) thus e <> c by A14; ::_thesis: b,e,c,d are_in_this_order_on P thus b,e,c,d are_in_this_order_on P by A7, A10, A15, Def1; ::_thesis: verum end; end; end; end; supposethat A17: ( LE d,a,P & LE a,b,P ) and A18: LE b,c,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A19: ( e <> b & e <> c ) and A20: ( LE b,e,P & LE e,c,P ) by A1, A18, Th8; take e ; ::_thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P ) thus ( e <> b & e <> c ) by A19; ::_thesis: b,e,c,d are_in_this_order_on P LE d,b,P by A17, JORDAN6:58; hence b,e,c,d are_in_this_order_on P by A20, Def1; ::_thesis: verum end; end; end; theorem :: JORDAN17:17 for P being Simple_closed_curve for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) let c, d, a, b be Point of (TOP-REAL 2); ::_thesis: ( c <> d & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) ) assume that A1: c <> d and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposethat A3: ( LE a,b,P & LE b,c,P ) and A4: LE c,d,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A5: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A4, Th8; take e ; ::_thesis: ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) LE a,c,P by A3, JORDAN6:58; hence ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) by A5, Def1; ::_thesis: verum end; supposethat A6: ( LE b,c,P & LE c,d,P ) and A7: LE d,a,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A8: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A6, Th8; take e ; ::_thesis: ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) thus ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) by A7, A8, Def1; ::_thesis: verum end; supposethat A9: LE c,d,P and A10: LE d,a,P and LE a,b,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A11: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A9, Th8; take e ; ::_thesis: ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) thus ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) by A10, A11, Def1; ::_thesis: verum end; supposethat A12: LE d,a,P and A13: LE a,b,P and A14: LE b,c,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) ::_thesis: verum proof A15: LE a,c,P by A13, A14, JORDAN6:58; percases ( d = W-min P or d <> W-min P ) ; supposeA16: d = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) c in P by A14, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A17: e <> c and A18: LE c,e,P by Th7; take e ; ::_thesis: ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) thus e <> c by A17; ::_thesis: ( e <> d & a,c,e,d are_in_this_order_on P ) thus e <> d by A1, A16, A18, JORDAN7:2; ::_thesis: a,c,e,d are_in_this_order_on P thus a,c,e,d are_in_this_order_on P by A12, A15, A18, Def1; ::_thesis: verum end; supposeA19: d <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> c & e <> d & a,c,e,d are_in_this_order_on P ) d in P by A12, JORDAN7:5; then A20: LE e,d,P by JORDAN7:3; now__::_thesis:_not_e_=_c LE d,b,P by A12, A13, JORDAN6:58; then A21: LE d,c,P by A14, JORDAN6:58; assume e = c ; ::_thesis: contradiction hence contradiction by A1, A20, A21, JORDAN6:57; ::_thesis: verum end; hence e <> c ; ::_thesis: ( e <> d & a,c,e,d are_in_this_order_on P ) thus e <> d by A19; ::_thesis: a,c,e,d are_in_this_order_on P thus a,c,e,d are_in_this_order_on P by A12, A15, A20, Def1; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:18 for P being Simple_closed_curve for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) let c, d, a, b be Point of (TOP-REAL 2); ::_thesis: ( c <> d & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) ) assume that A1: c <> d and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposethat A3: ( LE a,b,P & LE b,c,P ) and A4: LE c,d,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A5: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A4, Th8; take e ; ::_thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) thus ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) by A3, A5, Def1; ::_thesis: verum end; supposethat A6: LE b,c,P and A7: LE c,d,P and LE d,a,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A8: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A7, Th8; take e ; ::_thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) thus ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) by A6, A8, Def1; ::_thesis: verum end; supposethat A9: LE c,d,P and A10: ( LE d,a,P & LE a,b,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A11: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A9, Th8; take e ; ::_thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) LE d,b,P by A10, JORDAN6:58; hence ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) by A11, Def1; ::_thesis: verum end; supposethat A12: LE d,a,P and A13: LE a,b,P and A14: LE b,c,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) ::_thesis: verum proof A15: LE d,b,P by A12, A13, JORDAN6:58; percases ( d = W-min P or d <> W-min P ) ; supposeA16: d = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) c in P by A14, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A17: e <> c and A18: LE c,e,P by Th7; take e ; ::_thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) thus e <> c by A17; ::_thesis: ( e <> d & b,c,e,d are_in_this_order_on P ) thus e <> d by A1, A16, A18, JORDAN7:2; ::_thesis: b,c,e,d are_in_this_order_on P thus b,c,e,d are_in_this_order_on P by A14, A15, A18, Def1; ::_thesis: verum end; supposeA19: d <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) d in P by A12, JORDAN7:5; then A20: LE e,d,P by JORDAN7:3; now__::_thesis:_not_e_=_c assume A21: e = c ; ::_thesis: contradiction LE d,c,P by A14, A15, JORDAN6:58; hence contradiction by A1, A20, A21, JORDAN6:57; ::_thesis: verum end; hence e <> c ; ::_thesis: ( e <> d & b,c,e,d are_in_this_order_on P ) thus e <> d by A19; ::_thesis: b,c,e,d are_in_this_order_on P thus b,c,e,d are_in_this_order_on P by A14, A15, A20, Def1; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:19 for P being Simple_closed_curve for d, a, b, c being Point of (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for d, a, b, c being Point of (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) let d, a, b, c be Point of (TOP-REAL 2); ::_thesis: ( d <> a & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) ) assume that A1: d <> a and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposethat A3: LE a,b,P and A4: LE b,c,P and A5: LE c,d,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) ::_thesis: verum proof A6: LE b,d,P by A4, A5, JORDAN6:58; percases ( a = W-min P or a <> W-min P ) ; supposeA7: a = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) d in P by A5, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A8: e <> d and A9: LE d,e,P by Th7; take e ; ::_thesis: ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) thus e <> d by A8; ::_thesis: ( e <> a & a,b,d,e are_in_this_order_on P ) thus e <> a by A1, A7, A9, JORDAN7:2; ::_thesis: a,b,d,e are_in_this_order_on P thus a,b,d,e are_in_this_order_on P by A3, A6, A9, Def1; ::_thesis: verum end; supposeA10: a <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) a in P by A3, JORDAN7:5; then A11: LE e,a,P by JORDAN7:3; now__::_thesis:_not_e_=_d LE a,c,P by A3, A4, JORDAN6:58; then A12: LE a,d,P by A5, JORDAN6:58; assume e = d ; ::_thesis: contradiction hence contradiction by A1, A11, A12, JORDAN6:57; ::_thesis: verum end; hence e <> d ; ::_thesis: ( e <> a & a,b,d,e are_in_this_order_on P ) thus e <> a by A10; ::_thesis: a,b,d,e are_in_this_order_on P thus a,b,d,e are_in_this_order_on P by A3, A6, A11, Def1; ::_thesis: verum end; end; end; end; supposethat A13: ( LE b,c,P & LE c,d,P ) and A14: LE d,a,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A15: ( e <> d & e <> a & LE d,e,P & LE e,a,P ) by A1, A14, Th8; take e ; ::_thesis: ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) LE b,d,P by A13, JORDAN6:58; hence ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) by A15, Def1; ::_thesis: verum end; supposethat LE c,d,P and A16: LE d,a,P and A17: LE a,b,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A18: ( e <> d & e <> a & LE d,e,P & LE e,a,P ) by A1, A16, Th8; take e ; ::_thesis: ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) thus ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) by A17, A18, Def1; ::_thesis: verum end; supposethat A19: LE d,a,P and A20: LE a,b,P and LE b,c,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A21: ( e <> d & e <> a & LE d,e,P & LE e,a,P ) by A1, A19, Th8; take e ; ::_thesis: ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) thus ( e <> d & e <> a & a,b,d,e are_in_this_order_on P ) by A20, A21, Def1; ::_thesis: verum end; end; end; theorem :: JORDAN17:20 for P being Simple_closed_curve for d, a, b, c being Point of (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) proof let P be Simple_closed_curve; ::_thesis: for d, a, b, c being Point of (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) let d, a, b, c be Point of (TOP-REAL 2); ::_thesis: ( d <> a & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) ) assume that A1: d <> a and A2: ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def_1 ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A2; supposethat A3: LE a,b,P and A4: LE b,c,P and A5: LE c,d,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) thus ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) ::_thesis: verum proof A6: LE a,c,P by A3, A4, JORDAN6:58; percases ( a = W-min P or a <> W-min P ) ; supposeA7: a = W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) d in P by A5, JORDAN7:5; then consider e being Point of (TOP-REAL 2) such that A8: e <> d and A9: LE d,e,P by Th7; take e ; ::_thesis: ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) thus e <> d by A8; ::_thesis: ( e <> a & a,c,d,e are_in_this_order_on P ) thus e <> a by A1, A7, A9, JORDAN7:2; ::_thesis: a,c,d,e are_in_this_order_on P thus a,c,d,e are_in_this_order_on P by A5, A6, A9, Def1; ::_thesis: verum end; supposeA10: a <> W-min P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) take e = W-min P; ::_thesis: ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) a in P by A3, JORDAN7:5; then A11: LE e,a,P by JORDAN7:3; now__::_thesis:_not_e_=_d assume A12: e = d ; ::_thesis: contradiction LE a,d,P by A5, A6, JORDAN6:58; hence contradiction by A1, A11, A12, JORDAN6:57; ::_thesis: verum end; hence e <> d ; ::_thesis: ( e <> a & a,c,d,e are_in_this_order_on P ) thus e <> a by A10; ::_thesis: a,c,d,e are_in_this_order_on P thus a,c,d,e are_in_this_order_on P by A5, A6, A11, Def1; ::_thesis: verum end; end; end; end; supposethat LE b,c,P and A13: LE c,d,P and A14: LE d,a,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A15: ( e <> d & e <> a & LE d,e,P & LE e,a,P ) by A1, A14, Th8; take e ; ::_thesis: ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) thus ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) by A13, A15, Def1; ::_thesis: verum end; supposethat A16: LE c,d,P and A17: LE d,a,P and LE a,b,P ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A18: ( e <> d & e <> a & LE d,e,P & LE e,a,P ) by A1, A17, Th8; take e ; ::_thesis: ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) thus ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) by A16, A18, Def1; ::_thesis: verum end; supposethat A19: LE d,a,P and A20: ( LE a,b,P & LE b,c,P ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) consider e being Point of (TOP-REAL 2) such that A21: ( e <> d & e <> a & LE d,e,P & LE e,a,P ) by A1, A19, Th8; take e ; ::_thesis: ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) LE a,c,P by A20, JORDAN6:58; hence ( e <> d & e <> a & a,c,d,e are_in_this_order_on P ) by A21, Def1; ::_thesis: verum end; end; end; theorem :: JORDAN17:21 for P being Simple_closed_curve for a, c, d, b being Point of (TOP-REAL 2) st a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & b,a,c,d are_in_this_order_on P holds a = b proof let P be Simple_closed_curve; ::_thesis: for a, c, d, b being Point of (TOP-REAL 2) st a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & b,a,c,d are_in_this_order_on P holds a = b let a, c, d, b be Point of (TOP-REAL 2); ::_thesis: ( a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & b,a,c,d are_in_this_order_on P implies a = b ) assume that A1: a <> c and A2: a <> d and A3: b <> d and A4: a,b,c,d are_in_this_order_on P and A5: b,a,c,d are_in_this_order_on P ; ::_thesis: a = b percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4, Def1; supposeA6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: a = b then A7: LE b,d,P by JORDAN6:58; thus a = b ::_thesis: verum proof percases ( ( LE b,a,P & LE a,c,P & LE c,d,P ) or ( LE a,c,P & LE c,d,P & LE d,b,P ) or ( LE c,d,P & LE d,b,P & LE b,a,P ) or ( LE d,b,P & LE b,a,P & LE a,c,P ) ) by A5, Def1; suppose ( LE b,a,P & LE a,c,P & LE c,d,P ) ; ::_thesis: a = b hence a = b by A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,c,P & LE c,d,P & LE d,b,P ) ; ::_thesis: a = b hence a = b by A3, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,d,P & LE d,b,P & LE b,a,P ) ; ::_thesis: a = b hence a = b by A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,b,P & LE b,a,P & LE a,c,P ) ; ::_thesis: a = b hence a = b by A6, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA8: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: a = b then A9: LE b,d,P by JORDAN6:58; thus a = b ::_thesis: verum proof percases ( ( LE b,a,P & LE a,c,P & LE c,d,P ) or ( LE a,c,P & LE c,d,P & LE d,b,P ) or ( LE c,d,P & LE d,b,P & LE b,a,P ) or ( LE d,b,P & LE b,a,P & LE a,c,P ) ) by A5, Def1; supposeA10: ( LE b,a,P & LE a,c,P & LE c,d,P ) ; ::_thesis: a = b LE c,a,P by A8, JORDAN6:58; hence a = b by A1, A10, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,c,P & LE c,d,P & LE d,b,P ) ; ::_thesis: a = b hence a = b by A3, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,d,P & LE d,b,P & LE b,a,P ) ; ::_thesis: a = b hence a = b by A3, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,b,P & LE b,a,P & LE a,c,P ) ; ::_thesis: a = b hence a = b by A3, A9, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA11: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; ::_thesis: a = b then A12: LE c,a,P by JORDAN6:58; thus a = b ::_thesis: verum proof percases ( ( LE b,a,P & LE a,c,P & LE c,d,P ) or ( LE a,c,P & LE c,d,P & LE d,b,P ) or ( LE c,d,P & LE d,b,P & LE b,a,P ) or ( LE d,b,P & LE b,a,P & LE a,c,P ) ) by A5, Def1; suppose ( LE b,a,P & LE a,c,P & LE c,d,P ) ; ::_thesis: a = b hence a = b by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,c,P & LE c,d,P & LE d,b,P ) ; ::_thesis: a = b hence a = b by A1, A12, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,d,P & LE d,b,P & LE b,a,P ) ; ::_thesis: a = b hence a = b by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,b,P & LE b,a,P & LE a,c,P ) ; ::_thesis: a = b hence a = b by A11, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA13: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; ::_thesis: a = b thus a = b ::_thesis: verum proof percases ( ( LE b,a,P & LE a,c,P & LE c,d,P ) or ( LE a,c,P & LE c,d,P & LE d,b,P ) or ( LE c,d,P & LE d,b,P & LE b,a,P ) or ( LE d,b,P & LE b,a,P & LE a,c,P ) ) by A5, Def1; suppose ( LE b,a,P & LE a,c,P & LE c,d,P ) ; ::_thesis: a = b hence a = b by A13, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,c,P & LE c,d,P & LE d,b,P ) ; ::_thesis: a = b then LE a,d,P by JORDAN6:58; hence a = b by A2, A13, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,d,P & LE d,b,P & LE b,a,P ) ; ::_thesis: a = b hence a = b by A13, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,b,P & LE b,a,P & LE a,c,P ) ; ::_thesis: a = b hence a = b by A13, JORDAN6:57; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:22 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d are_in_this_order_on P holds a = c proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d are_in_this_order_on P holds a = c let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d are_in_this_order_on P implies a = c ) assume that A1: a <> b and A2: b <> c and A3: c <> d and A4: a,b,c,d are_in_this_order_on P and A5: c,b,a,d are_in_this_order_on P ; ::_thesis: a = c percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4, Def1; supposeA6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: a = c thus a = c ::_thesis: verum proof percases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5, Def1; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: a = c hence a = c by A1, A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: a = c hence a = c by A3, A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: a = c hence a = c by A3, A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: a = c hence a = c by A3, A6, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA7: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: a = c thus a = c ::_thesis: verum proof percases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5, Def1; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: a = c hence a = c by A2, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: a = c hence a = c by A3, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: a = c hence a = c by A3, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: a = c hence a = c by A3, A7, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA8: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; ::_thesis: a = c thus a = c ::_thesis: verum proof percases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5, Def1; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: a = c hence a = c by A1, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: a = c hence a = c by A3, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: a = c hence a = c by A3, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: a = c hence a = c by A3, A8, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA9: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; ::_thesis: a = c thus a = c ::_thesis: verum proof percases ( ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) or ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) ) by A5, Def1; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: a = c hence a = c by A2, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: a = c hence a = c by A1, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: a = c hence a = c by A2, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: a = c hence a = c by A1, A9, JORDAN6:57; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:23 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a are_in_this_order_on P holds a = d proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a are_in_this_order_on P holds a = d let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a are_in_this_order_on P implies a = d ) assume that A1: a <> b and A2: a <> c and A3: b <> d and A4: a,b,c,d are_in_this_order_on P and A5: d,b,c,a are_in_this_order_on P ; ::_thesis: a = d percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4, Def1; supposeA6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: a = d then A7: LE a,c,P by JORDAN6:58; thus a = d ::_thesis: verum proof percases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5, Def1; suppose ( LE d,b,P & LE b,c,P & LE c,a,P ) ; ::_thesis: a = d hence a = d by A2, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; ::_thesis: a = d hence a = d by A2, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; ::_thesis: a = d hence a = d by A2, A7, JORDAN6:57; ::_thesis: verum end; supposeA8: ( LE a,d,P & LE d,b,P & LE b,c,P ) ; ::_thesis: a = d LE b,d,P by A6, JORDAN6:58; hence a = d by A3, A8, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA9: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: a = d then A10: LE b,d,P by JORDAN6:58; thus a = d ::_thesis: verum proof percases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5, Def1; suppose ( LE d,b,P & LE b,c,P & LE c,a,P ) ; ::_thesis: a = d hence a = d by A3, A10, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; ::_thesis: a = d hence a = d by A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; ::_thesis: a = d hence a = d by A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,b,P & LE b,c,P ) ; ::_thesis: a = d hence a = d by A9, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA11: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; ::_thesis: a = d thus a = d ::_thesis: verum proof percases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5, Def1; suppose ( LE d,b,P & LE b,c,P & LE c,a,P ) ; ::_thesis: a = d then LE b,a,P by JORDAN6:58; hence a = d by A1, A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; ::_thesis: a = d hence a = d by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; ::_thesis: a = d hence a = d by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,b,P & LE b,c,P ) ; ::_thesis: a = d hence a = d by A11, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA12: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; ::_thesis: a = d thus a = d ::_thesis: verum proof percases ( ( LE d,b,P & LE b,c,P & LE c,a,P ) or ( LE b,c,P & LE c,a,P & LE a,d,P ) or ( LE c,a,P & LE a,d,P & LE d,b,P ) or ( LE a,d,P & LE d,b,P & LE b,c,P ) ) by A5, Def1; supposeA13: ( LE d,b,P & LE b,c,P & LE c,a,P ) ; ::_thesis: a = d LE a,c,P by A12, JORDAN6:58; hence a = d by A2, A13, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,c,P & LE c,a,P & LE a,d,P ) ; ::_thesis: a = d hence a = d by A12, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,a,P & LE a,d,P & LE d,b,P ) ; ::_thesis: a = d hence a = d by A12, JORDAN6:57; ::_thesis: verum end; suppose ( LE a,d,P & LE d,b,P & LE b,c,P ) ; ::_thesis: a = d hence a = d by A12, JORDAN6:57; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:24 for P being Simple_closed_curve for a, c, d, b being Point of (TOP-REAL 2) st a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & a,c,b,d are_in_this_order_on P holds b = c proof let P be Simple_closed_curve; ::_thesis: for a, c, d, b being Point of (TOP-REAL 2) st a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & a,c,b,d are_in_this_order_on P holds b = c let a, c, d, b be Point of (TOP-REAL 2); ::_thesis: ( a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & a,c,b,d are_in_this_order_on P implies b = c ) assume that A1: a <> c and A2: a <> d and A3: b <> d and A4: a,b,c,d are_in_this_order_on P and A5: a,c,b,d are_in_this_order_on P ; ::_thesis: b = c percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4, Def1; supposeA6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: b = c then A7: LE b,d,P by JORDAN6:58; thus b = c ::_thesis: verum proof percases ( ( LE a,c,P & LE c,b,P & LE b,d,P ) or ( LE c,b,P & LE b,d,P & LE d,a,P ) or ( LE b,d,P & LE d,a,P & LE a,c,P ) or ( LE d,a,P & LE a,c,P & LE c,b,P ) ) by A5, Def1; suppose ( LE a,c,P & LE c,b,P & LE b,d,P ) ; ::_thesis: b = c hence b = c by A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,d,P & LE d,a,P ) ; ::_thesis: b = c hence b = c by A6, JORDAN6:57; ::_thesis: verum end; supposeA8: ( LE b,d,P & LE d,a,P & LE a,c,P ) ; ::_thesis: b = c LE a,d,P by A6, A7, JORDAN6:58; hence b = c by A2, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,a,P & LE a,c,P & LE c,b,P ) ; ::_thesis: b = c hence b = c by A6, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA9: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: b = c then A10: LE c,a,P by JORDAN6:58; thus b = c ::_thesis: verum proof percases ( ( LE a,c,P & LE c,b,P & LE b,d,P ) or ( LE c,b,P & LE b,d,P & LE d,a,P ) or ( LE b,d,P & LE d,a,P & LE a,c,P ) or ( LE d,a,P & LE a,c,P & LE c,b,P ) ) by A5, Def1; suppose ( LE a,c,P & LE c,b,P & LE b,d,P ) ; ::_thesis: b = c hence b = c by A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,d,P & LE d,a,P ) ; ::_thesis: b = c hence b = c by A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,d,P & LE d,a,P & LE a,c,P ) ; ::_thesis: b = c hence b = c by A1, A10, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,a,P & LE a,c,P & LE c,b,P ) ; ::_thesis: b = c hence b = c by A9, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA11: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; ::_thesis: b = c then A12: LE c,a,P by JORDAN6:58; thus b = c ::_thesis: verum proof percases ( ( LE a,c,P & LE c,b,P & LE b,d,P ) or ( LE c,b,P & LE b,d,P & LE d,a,P ) or ( LE b,d,P & LE d,a,P & LE a,c,P ) or ( LE d,a,P & LE a,c,P & LE c,b,P ) ) by A5, Def1; suppose ( LE a,c,P & LE c,b,P & LE b,d,P ) ; ::_thesis: b = c hence b = c by A1, A12, JORDAN6:57; ::_thesis: verum end; supposeA13: ( LE c,b,P & LE b,d,P & LE d,a,P ) ; ::_thesis: b = c LE d,b,P by A11, JORDAN6:58; hence b = c by A3, A13, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,d,P & LE d,a,P & LE a,c,P ) ; ::_thesis: b = c hence b = c by A1, A12, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,a,P & LE a,c,P & LE c,b,P ) ; ::_thesis: b = c hence b = c by A1, A12, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA14: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; ::_thesis: b = c thus b = c ::_thesis: verum proof percases ( ( LE a,c,P & LE c,b,P & LE b,d,P ) or ( LE c,b,P & LE b,d,P & LE d,a,P ) or ( LE b,d,P & LE d,a,P & LE a,c,P ) or ( LE d,a,P & LE a,c,P & LE c,b,P ) ) by A5, Def1; suppose ( LE a,c,P & LE c,b,P & LE b,d,P ) ; ::_thesis: b = c hence b = c by A14, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,d,P & LE d,a,P ) ; ::_thesis: b = c hence b = c by A14, JORDAN6:57; ::_thesis: verum end; supposeA15: ( LE b,d,P & LE d,a,P & LE a,c,P ) ; ::_thesis: b = c LE d,b,P by A14, JORDAN6:58; hence b = c by A3, A15, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,a,P & LE a,c,P & LE c,b,P ) ; ::_thesis: b = c hence b = c by A14, JORDAN6:57; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:25 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b are_in_this_order_on P holds b = d proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b are_in_this_order_on P holds b = d let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b are_in_this_order_on P implies b = d ) assume that A1: a <> b and A2: b <> c and A3: c <> d and A4: a,b,c,d are_in_this_order_on P and A5: a,d,c,b are_in_this_order_on P ; ::_thesis: b = d percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4, Def1; supposeA6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: b = d thus b = d ::_thesis: verum proof percases ( ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) or ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) ) by A5, Def1; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: b = d hence b = d by A2, A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: b = d hence b = d by A3, A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: b = d hence b = d by A2, A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: b = d hence b = d by A3, A6, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA7: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: b = d thus b = d ::_thesis: verum proof percases ( ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) or ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) ) by A5, Def1; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: b = d hence b = d by A3, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: b = d hence b = d by A3, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: b = d hence b = d by A2, A7, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: b = d hence b = d by A3, A7, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA8: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; ::_thesis: b = d thus b = d ::_thesis: verum proof percases ( ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) or ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) ) by A5, Def1; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: b = d hence b = d by A3, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: b = d hence b = d by A1, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: b = d hence b = d by A1, A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: b = d hence b = d by A1, A8, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA9: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; ::_thesis: b = d thus b = d ::_thesis: verum proof percases ( ( LE a,d,P & LE d,c,P & LE c,b,P ) or ( LE d,c,P & LE c,b,P & LE b,a,P ) or ( LE c,b,P & LE b,a,P & LE a,d,P ) or ( LE b,a,P & LE a,d,P & LE d,c,P ) ) by A5, Def1; suppose ( LE a,d,P & LE d,c,P & LE c,b,P ) ; ::_thesis: b = d hence b = d by A2, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,b,P & LE b,a,P ) ; ::_thesis: b = d hence b = d by A2, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,b,P & LE b,a,P & LE a,d,P ) ; ::_thesis: b = d hence b = d by A2, A9, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,a,P & LE a,d,P & LE d,c,P ) ; ::_thesis: b = d hence b = d by A1, A9, JORDAN6:57; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:26 for P being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c are_in_this_order_on P holds c = d proof let P be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c are_in_this_order_on P holds c = d let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c are_in_this_order_on P implies c = d ) assume that A1: a <> b and A2: a <> c and A3: b <> d and A4: a,b,c,d are_in_this_order_on P and A5: a,b,d,c are_in_this_order_on P ; ::_thesis: c = d percases ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) by A4, Def1; supposeA6: ( LE a,b,P & LE b,c,P & LE c,d,P ) ; ::_thesis: c = d thus c = d ::_thesis: verum proof percases ( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) ) by A5, Def1; suppose ( LE a,b,P & LE b,d,P & LE d,c,P ) ; ::_thesis: c = d hence c = d by A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,d,P & LE d,c,P & LE c,a,P ) ; ::_thesis: c = d hence c = d by A6, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,a,P & LE a,b,P ) ; ::_thesis: c = d hence c = d by A6, JORDAN6:57; ::_thesis: verum end; supposeA7: ( LE c,a,P & LE a,b,P & LE b,d,P ) ; ::_thesis: c = d LE a,c,P by A6, JORDAN6:58; hence c = d by A2, A7, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA8: ( LE b,c,P & LE c,d,P & LE d,a,P ) ; ::_thesis: c = d then A9: LE c,a,P by JORDAN6:58; thus c = d ::_thesis: verum proof percases ( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) ) by A5, Def1; suppose ( LE a,b,P & LE b,d,P & LE d,c,P ) ; ::_thesis: c = d hence c = d by A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,d,P & LE d,c,P & LE c,a,P ) ; ::_thesis: c = d hence c = d by A8, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,a,P & LE a,b,P ) ; ::_thesis: c = d hence c = d by A8, JORDAN6:57; ::_thesis: verum end; supposeA10: ( LE c,a,P & LE a,b,P & LE b,d,P ) ; ::_thesis: c = d LE b,a,P by A8, A9, JORDAN6:58; hence c = d by A1, A10, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA11: ( LE c,d,P & LE d,a,P & LE a,b,P ) ; ::_thesis: c = d then A12: LE d,b,P by JORDAN6:58; thus c = d ::_thesis: verum proof percases ( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) ) by A5, Def1; suppose ( LE a,b,P & LE b,d,P & LE d,c,P ) ; ::_thesis: c = d hence c = d by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,d,P & LE d,c,P & LE c,a,P ) ; ::_thesis: c = d hence c = d by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE d,c,P & LE c,a,P & LE a,b,P ) ; ::_thesis: c = d hence c = d by A11, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,a,P & LE a,b,P & LE b,d,P ) ; ::_thesis: c = d hence c = d by A3, A12, JORDAN6:57; ::_thesis: verum end; end; end; end; supposeA13: ( LE d,a,P & LE a,b,P & LE b,c,P ) ; ::_thesis: c = d then A14: LE d,b,P by JORDAN6:58; thus c = d ::_thesis: verum proof percases ( ( LE a,b,P & LE b,d,P & LE d,c,P ) or ( LE b,d,P & LE d,c,P & LE c,a,P ) or ( LE d,c,P & LE c,a,P & LE a,b,P ) or ( LE c,a,P & LE a,b,P & LE b,d,P ) ) by A5, Def1; suppose ( LE a,b,P & LE b,d,P & LE d,c,P ) ; ::_thesis: c = d hence c = d by A3, A14, JORDAN6:57; ::_thesis: verum end; suppose ( LE b,d,P & LE d,c,P & LE c,a,P ) ; ::_thesis: c = d hence c = d by A3, A14, JORDAN6:57; ::_thesis: verum end; supposeA15: ( LE d,c,P & LE c,a,P & LE a,b,P ) ; ::_thesis: c = d LE a,c,P by A13, JORDAN6:58; hence c = d by A2, A15, JORDAN6:57; ::_thesis: verum end; suppose ( LE c,a,P & LE a,b,P & LE b,d,P ) ; ::_thesis: c = d hence c = d by A3, A14, JORDAN6:57; ::_thesis: verum end; end; end; end; end; end; theorem :: JORDAN17:27 for C being Simple_closed_curve for a, b, c, d being Point of (TOP-REAL 2) st a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C holds a,d,c,b are_in_this_order_on C proof let C be Simple_closed_curve; ::_thesis: for a, b, c, d being Point of (TOP-REAL 2) st a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C holds a,d,c,b are_in_this_order_on C let a, b, c, d be Point of (TOP-REAL 2); ::_thesis: ( a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C implies a,d,c,b are_in_this_order_on C ) assume that A1: a in C and A2: b in C and A3: c in C and A4: d in C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) percases ( ( LE a,b,C & LE b,c,C & LE c,d,C ) or ( LE a,b,C & LE b,c,C & not LE c,d,C ) or ( LE a,b,C & not LE b,c,C & LE c,d,C ) or ( LE a,b,C & not LE b,c,C & not LE c,d,C ) or ( not LE a,b,C & LE b,c,C & LE c,d,C ) or ( not LE a,b,C & LE b,c,C & not LE c,d,C ) or ( not LE a,b,C & not LE b,c,C & LE c,d,C ) or ( not LE a,b,C & not LE b,c,C & not LE c,d,C ) ) ; suppose ( LE a,b,C & LE b,c,C & LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by Def1; ::_thesis: verum end; supposeA5: ( LE a,b,C & LE b,c,C & not LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A6: LE d,c,C by A3, A4, JORDAN16:7; thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7; supposeA7: LE a,d,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A5, A6, A7, Def1; ::_thesis: verum end; suppose LE d,a,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A5, Def1; ::_thesis: verum end; end; end; end; supposeA8: ( LE a,b,C & not LE b,c,C & LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A9: LE c,b,C by A2, A3, JORDAN16:7; thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7; supposeA10: LE b,d,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A8, A9, A10, Def1; ::_thesis: verum end; supposeA11: LE d,b,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7; suppose LE a,c,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A8, A11, Def1; ::_thesis: verum end; supposeA12: LE c,a,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A8, A11, A12, Def1; ::_thesis: verum end; end; end; end; end; end; end; supposeA13: ( LE a,b,C & not LE b,c,C & not LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A14: LE d,c,C by A3, A4, JORDAN16:7; A15: LE c,b,C by A2, A3, A13, JORDAN16:7; thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7; supposeA16: LE a,c,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A15, A14, A16, Def1; ::_thesis: verum end; suppose LE c,a,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A13, A14, Def1; ::_thesis: verum end; end; end; end; supposeA17: ( not LE a,b,C & LE b,c,C & LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A18: LE b,a,C by A1, A2, JORDAN16:7; thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7; supposeA19: LE a,d,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A17, A18, A19, Def1; ::_thesis: verum end; suppose LE d,a,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A17, Def1; ::_thesis: verum end; end; end; end; supposeA20: ( not LE a,b,C & LE b,c,C & not LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A21: ( LE b,a,C & LE d,c,C ) by A1, A2, A3, A4, JORDAN16:7; thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7; suppose LE a,d,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A21, Def1; ::_thesis: verum end; supposeA22: LE d,a,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) A23: ( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7; ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A20, A21, A22, A23, Def1; ::_thesis: verum end; end; end; end; supposeA24: ( not LE a,b,C & not LE b,c,C & LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A25: ( LE b,a,C & LE c,b,C ) by A1, A2, A3, JORDAN16:7; thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ::_thesis: verum proof percases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7; suppose LE a,d,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A25, Def1; ::_thesis: verum end; supposeA26: LE d,a,C ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A24, A25, A26, Def1; ::_thesis: verum end; end; end; end; supposeA27: ( not LE a,b,C & not LE b,c,C & not LE c,d,C ) ; ::_thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) then A28: LE d,c,C by A3, A4, JORDAN16:7; ( LE b,a,C & LE c,b,C ) by A1, A2, A3, A27, JORDAN16:7; hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A28, Def1; ::_thesis: verum end; end; end;