A25: not q in {q1} by A22, TARSKI:def 1;
not q2 in {q1} by A5, TARSKI:def 1;
then reconsider Qa = P \ {q1} as non empty Subset of ((TOP-REAL 2) | P) by A7, A16, XBOOLE_0:def 5, XBOOLE_1:36;
A26: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:8;
reconsider Qa9 = Qa as Subset of (TOP-REAL 2) ;
A27: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:8;
A28: Segment (Q1,q1,q2,q,q2) is_an_arc_of q,q2 by A2, A20, A21, A19, Th21;
then consider f2 being Function of I[01],((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2))) such that
A29: f2 is being_homeomorphism and
A30: ( f2 . 0 = q & f2 . 1 = q2 ) by TOPREAL1:def 1;
A31: rng f2 = [#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q,q2))) by A29, TOPS_2:def 5
.= Segment (Q1,q1,q2,q,q2) by PRE_TOPC:def 5 ;
A32: ( not p2 in {q1} & not q2 in {q1} ) by A5, A8, TARSKI:def 1;
q in { p3 where p3 is Point of (TOP-REAL 2) : ( LE p1,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) } by A24, JORDAN6:26;
then A33: ex p3 being Point of (TOP-REAL 2) st
( q = p3 & LE p1,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) ;
then not p1 in {q1} by TARSKI:def 1;
then reconsider p19 = p1, q9 = q, q29 = q2, p29 = p2 as Point of (((TOP-REAL 2) | P) | Qa) by A4, A7, A13, A20, A26, A32, A25, XBOOLE_0:def 5;
then consider G1 being Path of p19,q9 such that
A55: ( G1 is continuous & G1 . 0 = p19 & G1 . 1 = q9 ) ;
then consider G3 being Path of q29,p29 such that
A76: ( G3 is continuous & G3 . 0 = q29 & G3 . 1 = p29 ) ;
{ p where p is Point of (TOP-REAL 2) : ( LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) } c= Qa then A80: Segment (Q1,q1,q2,q,q2) c= Qa by JORDAN6:26;
dom f2 = the carrier of I[01] by A18, A29, TOPS_2:def 5;
then reconsider g2 = f2 as Function of I[01],(((TOP-REAL 2) | P) | Qa) by A31, A27, A80, FUNCT_2:2;
A81: f2 is continuous by A29, TOPS_2:def 5;
A82: for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g2 " G is open [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
then A90: g2 is continuous by A82, TOPS_2:43;
then q9,q29 are_connected by A30, BORSUK_2:def 1;
then reconsider G2 = g2 as Path of q9,q29 by A30, A90, BORSUK_2:def 2;
A91: (G1 + G2) . 1 = q29 by A55, A30, A90, BORSUK_2:14;
A92: ( G1 + G2 is continuous & (G1 + G2) . 0 = p19 ) by A55, A30, A90, BORSUK_2:14;
then A93: ((G1 + G2) + G3) . 1 = p29 by A91, A76, BORSUK_2:14;
( (G1 + G2) + G3 is continuous & ((G1 + G2) + G3) . 0 = p19 ) by A92, A91, A76, BORSUK_2:14;
hence contradiction by A1, A10, A8, A34, A93, Th18; :: thesis: verum

A95: ( not p1 in {q2} & not q1 in {q2} ) by A5, A11, TARSKI:def 1;
not q1 in {q2} by A5, TARSKI:def 1;
then reconsider Qa = P \ {q2} as non empty Subset of ((TOP-REAL 2) | P) by A10, A16, XBOOLE_0:def 5, XBOOLE_1:36;
A96: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:8;
reconsider Qa9 = Qa as Subset of (TOP-REAL 2) ;
A97: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:8;
A98: Segment (Q1,q1,q2,q1,q) is_an_arc_of q1,q by A2, A20, A22, JORDAN16:24;
then consider f2 being Function of I[01],((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q))) such that
A99: f2 is being_homeomorphism and
A100: ( f2 . 0 = q1 & f2 . 1 = q ) by TOPREAL1:def 1;
A101: rng f2 = [#] ((TOP-REAL 2) | (Segment (Q1,q1,q2,q1,q))) by A99, TOPS_2:def 5
.= Segment (Q1,q1,q2,q1,q) by PRE_TOPC:def 5 ;
A102: not q in {q2} by A21, A19, TARSKI:def 1;
q in { p3 where p3 is Point of (TOP-REAL 2) : ( LE q2,p3,P,p1,p2 & LE p3,p2,P,p1,p2 ) } by A94, JORDAN6:26;
then A103: ex p3 being Point of (TOP-REAL 2) st
( q = p3 & LE q2,p3,P,p1,p2 & LE p3,p2,P,p1,p2 ) ;
then not p2 in {q2} by TARSKI:def 1;
then reconsider p19 = p1, q9 = q, q19 = q1, p29 = p2 as Point of (((TOP-REAL 2) | P) | Qa) by A4, A10, A13, A20, A96, A95, A102, XBOOLE_0:def 5;
then consider G1 being Path of q9,p29 such that
A125: ( G1 is continuous & G1 . 0 = q9 & G1 . 1 = p29 ) ;
then consider G3 being Path of p19,q19 such that
A146: ( G3 is continuous & G3 . 0 = p19 & G3 . 1 = q19 ) ;
{ p where p is Point of (TOP-REAL 2) : ( LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) } c= Qa then A150: Segment (Q1,q1,q2,q1,q) c= Qa by JORDAN6:26;
dom f2 = the carrier of I[01] by A18, A99, TOPS_2:def 5;
then reconsider g2 = f2 as Function of I[01],(((TOP-REAL 2) | P) | Qa) by A101, A97, A150, FUNCT_2:2;
A151: f2 is continuous by A99, TOPS_2:def 5;
A152: for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g2 " G is open [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
then A160: g2 is continuous by A152, TOPS_2:43;
then q19,q9 are_connected by A100, BORSUK_2:def 1;
then reconsider G2 = g2 as Path of q19,q9 by A100, A160, BORSUK_2:def 2;
A161: (G2 + G1) . 1 = p29 by A125, A100, A160, BORSUK_2:14;
A162: ( G2 + G1 is continuous & (G2 + G1) . 0 = q19 ) by A125, A100, A160, BORSUK_2:14;
then A163: (G3 + (G2 + G1)) . 1 = p29 by A161, A146, BORSUK_2:14;
( G3 + (G2 + G1) is continuous & (G3 + (G2 + G1)) . 0 = p19 ) by A162, A161, A146, BORSUK_2:14;
hence contradiction by A1, A7, A11, A104, A163, Th18; :: thesis: verum