let P, Q1 be non empty Subset of (TOP-REAL 2); :: thesis:
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis:
assume A1: ( P is_an_arc_of p1,p2 & Q1 is_an_arc_of q1,q2 & LE q1,q2,P,p1,p2 & Q1 c= P ) ; :: thesis:
then A2: q1 in P by JORDAN5C:def 3;
A3: q2 in P by A1, JORDAN5C:def 3;
A4: ( p1 in P & p2 in P ) by A1, TOPREAL1:4;
A5: q1 <> q2 by A1, JORDAN6:49;
then A6: Segment P,p1,p2,q1,q2 is_an_arc_of q1,q2 by A1, JORDAN16:36;

A7: now

assume A8: q1 = p2 ; :: thesis:
LE q2,p2,P,p1,p2 by A1, A3, JORDAN5C:10;
hence contradiction by A1, A8, JORDAN5C:12, JORDAN6:49; :: thesis:

end;

A9: now

assume A10: q2 = p1 ; :: thesis:
LE p1,q1,P,p1,p2 by A1, A2, JORDAN5C:10;
hence contradiction by A1, A10, JORDAN5C:12, JORDAN6:49; :: thesis:

end;

reconsider Q0 = Segment P,p1,p2,q1,q2 as non empty Subset of (TOP-REAL 2) by A1, JORDAN16:22;

now

assume not Q1 c= Q0 ; :: thesis:
then consider x8 being set such that
A11: ( x8 in Q1 & not x8 in Q0 ) by TARSKI:def 3;
Q0 is_an_arc_of q1,q2 by A1, A5, JORDAN16:36;
then A12: ( q1 in Q0 & q2 in Q0 ) by TOPREAL1:4;
reconsider q = x8 as Point of (TOP-REAL 2) by A11;
A13: q <> q1 by A1, A11, JORDAN16:9;
A14: [#] I[01] = the carrier of I[01] ;
A15: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 10;
A16: LE p1,q1,P,p1,p2 by A1, A2, JORDAN5C:10;
then A17: (Segment P,p1,p2,p1,q1) \/ (Segment P,p1,p2,q1,q2) = Segment P,p1,p2,p1,q2 by A1, Th23;
A18: LE p1,q2,P,p1,p2 by A1, A16, JORDAN5C:13;
LE q2,p2,P,p1,p2 by A1, A3, JORDAN5C:10;
then (Segment P,p1,p2,p1,q2) \/ (Segment P,p1,p2,q2,p2) = Segment P,p1,p2,p1,p2 by A1, A18, Th23
.= P by A1, Th25 ;
then A19: ( q in Segment P,p1,p2,p1,q2 or q in Segment P,p1,p2,q2,p2 ) by A1, A11, XBOOLE_0:def 3;

now

per cases by A11, A17, A19, XBOOLE_0:def 3;

case q in Segment P,p1,p2,p1,q1 ; :: thesis:

then q in { p3 where p3 is Point of (TOP-REAL 2) : ( LE p1,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) } by JORDAN6:29;
then consider p3 being Point of (TOP-REAL 2) such that
A20: ( q = p3 & LE p1,p3,P,p1,p2 & LE p3,q1,P,p1,p2 ) ;
not q2 in {q1} by A5, TARSKI:def 1;
then reconsider Qa = P \ {q1} as non empty Subset of ((TOP-REAL 2) | P) by A3, A15, XBOOLE_0:def 5, XBOOLE_1:36;
reconsider Qa' = Qa as Subset of (TOP-REAL 2) ;

A21: now

assume A22: p1 = q1 ; :: thesis:
then q = p1 by A1, A20, JORDAN5C:12;
hence contradiction by A6, A11, A22, TOPREAL1:4; :: thesis:

end;

A23: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:29;
A24: not p1 in {q1} by A21, TARSKI:def 1;
A25: not p2 in {q1} by A7, TARSKI:def 1;
A26: not q2 in {q1} by A5, TARSKI:def 1;
not q in {q1} by A13, TARSKI:def 1;
then reconsider p1' = p1, q' = q, q2' = q2, p2' = p2 as Point of (((TOP-REAL 2) | P) | Qa) by A1, A3, A4, A11, A23, A24, A25, A26, XBOOLE_0:def 5;

now

per cases ;

case q <> p1 ; :: thesis:

then A27: Segment P,p1,p2,p1,q is_an_arc_of p1,q by A1, A11, JORDAN16:39;
then consider f1 being Function of I[01] ,((TOP-REAL 2) | (Segment P,p1,p2,p1,q)) such that
A28: ( f1 is being_homeomorphism & f1 . 0 = p1 & f1 . 1 = q ) by TOPREAL1:def 2;
A29: f1 is continuous by A28, TOPS_2:def 5;
A30: dom f1 = the carrier of I[01] by A14, A28, TOPS_2:def 5;
A31: rng f1 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q)) by A28, TOPS_2:def 5
.= Segment P,p1,p2,p1,q by PRE_TOPC:def 10 ;
{ p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q,P,p1,p2 ) } c= Qa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q,P,p1,p2 ) } ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A32: ( x = p & LE p1,p,P,p1,p2 & LE p,q,P,p1,p2 ) ;
x <> q1 by A1, A13, A20, A32, JORDAN5C:12;
then ( x in P & not x in {q1} ) by A32, JORDAN5C:def 3, TARSKI:def 1;
hence x in Qa by XBOOLE_0:def 5; :: thesis:

end;

then A33: Segment P,p1,p2,p1,q c= Qa by JORDAN6:29;
then reconsider g1 = f1 as Function of I[01] ,(((TOP-REAL 2) | P) | Qa) by A23, A30, A31, FUNCT_2:4;
A34: [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g1 " G is open

proof

let G be Subset of (((TOP-REAL 2) | P) | Qa); :: thesis:
assume A35: G is open ; :: thesis:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa' by PRE_TOPC:28, XBOOLE_1:36;
then consider G4 being Subset of (TOP-REAL 2) such that
A36: ( G4 is open & G = G4 /\ ([#] ((TOP-REAL 2) | Qa')) ) by A35, TOPS_2:32;
reconsider G5 = G4 /\ ([#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q))) as Subset of ((TOP-REAL 2) | (Segment P,p1,p2,p1,q)) ;
p1 in Segment P,p1,p2,p1,q by A27, TOPREAL1:4;
then A37: not [#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q)) is empty ;
A38: G5 is open by A36, TOPS_2:32;
A39: f1 " G5 = g1 " (G4 /\ (Segment P,p1,p2,p1,q)) by PRE_TOPC:def 10
.= (g1 " G4) /\ (g1 " (Segment P,p1,p2,p1,q)) by FUNCT_1:137 ;
A40: rng g1 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q)) by A28, TOPS_2:def 5
.= Segment P,p1,p2,p1,q by PRE_TOPC:def 10 ;
g1 " G = (g1 " G4) /\ (g1 " ([#] ((TOP-REAL 2) | Qa'))) by A36, FUNCT_1:137
.= (g1 " G4) /\ (g1 " Qa') by PRE_TOPC:def 10
.= (g1 " G4) /\ (g1 " ((rng g1) /\ Qa')) by RELAT_1:168
.= (g1 " G4) /\ (g1 " (Segment P,p1,p2,p1,q)) by A33, A40, XBOOLE_1:28 ;
hence g1 " G is open by A29, A37, A38, A39, TOPS_2:55; :: thesis:

end;

then A41: g1 is continuous by A34, TOPS_2:55;
then p1',q' are_connected by A28, BORSUK_2:def 1;
then g1 is Path of p1',q' by A28, A41, BORSUK_2:def 2;
hence ex G1 being Path of p1',q' st
( G1 is continuous & G1 . 0 = p1' & G1 . 1 = q' ) by A28, A41; :: thesis:

end;

case A42: q = p1 ; :: thesis:

consider g01 being Function of I[01] ,(((TOP-REAL 2) | P) | Qa) such that
A43: ( g01 is continuous & g01 . 0 = p1' & g01 . 1 = p1' ) by BORSUK_2:4;
p1',p1' are_connected ;
then g01 is Path of p1',p1' by A43, BORSUK_2:def 2;
hence ex G1 being Path of p1',q' st
( G1 is continuous & G1 . 0 = p1' & G1 . 1 = q' ) by A42, A43; :: thesis:

end;

then consider G1 being Path of p1',q' such that
A44: ( G1 is continuous & G1 . 0 = p1' & G1 . 1 = q' ) ;
A45: Segment Q1,q1,q2,q,q2 is_an_arc_of q,q2 by A1, A11, A12, Th22;
then consider f2 being Function of I[01] ,((TOP-REAL 2) | (Segment Q1,q1,q2,q,q2)) such that
A46: ( f2 is being_homeomorphism & f2 . 0 = q & f2 . 1 = q2 ) by TOPREAL1:def 2;
A47: f2 is continuous by A46, TOPS_2:def 5;
A48: dom f2 = the carrier of I[01] by A14, A46, TOPS_2:def 5;
A49: rng f2 = [#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q,q2)) by A46, TOPS_2:def 5
.= Segment Q1,q1,q2,q,q2 by PRE_TOPC:def 10 ;
A50: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:29;
{ p where p is Point of (TOP-REAL 2) : ( LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) } c= Qa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) } ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A51: ( x = p & LE q,p,Q1,q1,q2 & LE p,q2,Q1,q1,q2 ) ;
A52: x in Q1 by A51, JORDAN5C:def 3;

now

assume A53: x = q1 ; :: thesis:
LE q1,q,Q1,q1,q2 by A1, A11, JORDAN5C:10;
hence contradiction by A1, A13, A51, A53, JORDAN5C:12; :: thesis:

end;

then ( x in P & not x in {q1} ) by A1, A52, TARSKI:def 1;
hence x in Qa by XBOOLE_0:def 5; :: thesis:

end;

then A54: Segment Q1,q1,q2,q,q2 c= Qa by JORDAN6:29;
then reconsider g2 = f2 as Function of I[01] ,(((TOP-REAL 2) | P) | Qa) by A48, A49, A50, FUNCT_2:4;
A55: [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g2 " G is open

proof

let G be Subset of (((TOP-REAL 2) | P) | Qa); :: thesis:
assume A56: G is open ; :: thesis:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa' by PRE_TOPC:28, XBOOLE_1:36;
then consider G4 being Subset of (TOP-REAL 2) such that
A57: ( G4 is open & G = G4 /\ ([#] ((TOP-REAL 2) | Qa')) ) by A56, TOPS_2:32;
reconsider G5 = G4 /\ ([#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q,q2))) as Subset of ((TOP-REAL 2) | (Segment Q1,q1,q2,q,q2)) ;
q2 in Segment Q1,q1,q2,q,q2 by A45, TOPREAL1:4;
then A58: not [#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q,q2)) is empty ;
A59: G5 is open by A57, TOPS_2:32;
A60: f2 " G5 = g2 " (G4 /\ (Segment Q1,q1,q2,q,q2)) by PRE_TOPC:def 10
.= (g2 " G4) /\ (g2 " (Segment Q1,q1,q2,q,q2)) by FUNCT_1:137 ;
A61: rng g2 = [#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q,q2)) by A46, TOPS_2:def 5
.= Segment Q1,q1,q2,q,q2 by PRE_TOPC:def 10 ;
g2 " G = (g2 " G4) /\ (g2 " ([#] ((TOP-REAL 2) | Qa'))) by A57, FUNCT_1:137
.= (g2 " G4) /\ (g2 " Qa') by PRE_TOPC:def 10
.= (g2 " G4) /\ (g2 " ((rng g2) /\ Qa')) by RELAT_1:168
.= (g2 " G4) /\ (g2 " (Segment Q1,q1,q2,q,q2)) by A54, A61, XBOOLE_1:28 ;
hence g2 " G is open by A47, A58, A59, A60, TOPS_2:55; :: thesis:

end;

then A62: g2 is continuous by A55, TOPS_2:55;
then q',q2' are_connected by A46, BORSUK_2:def 1;
then reconsider G2 = g2 as Path of q',q2' by A46, A62, BORSUK_2:def 2;
A63: ( G1 + G2 is continuous & (G1 + G2) . 0 = p1' & (G1 + G2) . 1 = q2' ) by A44, A46, A62, BORSUK_2:17;

now

per cases ;

case q2 <> p2 ; :: thesis:

then A64: Segment P,p1,p2,q2,p2 is_an_arc_of q2,p2 by A1, A3, Th22;
then consider f3 being Function of I[01] ,((TOP-REAL 2) | (Segment P,p1,p2,q2,p2)) such that
A65: ( f3 is being_homeomorphism & f3 . 0 = q2 & f3 . 1 = p2 ) by TOPREAL1:def 2;
A66: f3 is continuous by A65, TOPS_2:def 5;
A67: dom f3 = the carrier of I[01] by A14, A65, TOPS_2:def 5;
A68: rng f3 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,q2,p2)) by A65, TOPS_2:def 5
.= Segment P,p1,p2,q2,p2 by PRE_TOPC:def 10 ;
A69: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:29;
{ p where p is Point of (TOP-REAL 2) : ( LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } c= Qa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A70: ( x = p & LE q2,p,P,p1,p2 & LE p,p2,P,p1,p2 ) ;
x <> q1 by A1, A70, JORDAN5C:12, JORDAN6:49;
then ( x in P & not x in {q1} ) by A70, JORDAN5C:def 3, TARSKI:def 1;
hence x in Qa by XBOOLE_0:def 5; :: thesis:

end;

then A71: Segment P,p1,p2,q2,p2 c= Qa by JORDAN6:29;
then reconsider g3 = f3 as Function of I[01] ,(((TOP-REAL 2) | P) | Qa) by A67, A68, A69, FUNCT_2:4;
A72: [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g3 " G is open

proof

let G be Subset of (((TOP-REAL 2) | P) | Qa); :: thesis:
assume A73: G is open ; :: thesis:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa' by PRE_TOPC:28, XBOOLE_1:36;
then consider G4 being Subset of (TOP-REAL 2) such that
A74: ( G4 is open & G = G4 /\ ([#] ((TOP-REAL 2) | Qa')) ) by A73, TOPS_2:32;
reconsider G5 = G4 /\ ([#] ((TOP-REAL 2) | (Segment P,p1,p2,q2,p2))) as Subset of ((TOP-REAL 2) | (Segment P,p1,p2,q2,p2)) ;
p2 in Segment P,p1,p2,q2,p2 by A64, TOPREAL1:4;
then A75: not [#] ((TOP-REAL 2) | (Segment P,p1,p2,q2,p2)) is empty ;
A76: G5 is open by A74, TOPS_2:32;
A77: f3 " G5 = g3 " (G4 /\ (Segment P,p1,p2,q2,p2)) by PRE_TOPC:def 10
.= (g3 " G4) /\ (g3 " (Segment P,p1,p2,q2,p2)) by FUNCT_1:137 ;
A78: rng g3 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,q2,p2)) by A65, TOPS_2:def 5
.= Segment P,p1,p2,q2,p2 by PRE_TOPC:def 10 ;
g3 " G = (g3 " G4) /\ (g3 " ([#] ((TOP-REAL 2) | Qa'))) by A74, FUNCT_1:137
.= (g3 " G4) /\ (g3 " Qa') by PRE_TOPC:def 10
.= (g3 " G4) /\ (g3 " ((rng g3) /\ Qa')) by RELAT_1:168
.= (g3 " G4) /\ (g3 " (Segment P,p1,p2,q2,p2)) by A71, A78, XBOOLE_1:28 ;
hence g3 " G is open by A66, A75, A76, A77, TOPS_2:55; :: thesis:

end;

then A79: g3 is continuous by A72, TOPS_2:55;
then q2',p2' are_connected by A65, BORSUK_2:def 1;
then g3 is Path of q2',p2' by A65, A79, BORSUK_2:def 2;
hence ex G3 being Path of q2',p2' st
( G3 is continuous & G3 . 0 = q2' & G3 . 1 = p2' ) by A65, A79; :: thesis:

end;

case A80: q2 = p2 ; :: thesis:

consider g01 being Function of I[01] ,(((TOP-REAL 2) | P) | Qa) such that
A81: ( g01 is continuous & g01 . 0 = q2' & g01 . 1 = q2' ) by BORSUK_2:4;
q2',q2' are_connected ;
then g01 is Path of q2',q2' by A81, BORSUK_2:def 2;
hence ex G3 being Path of q2',p2' st
( G3 is continuous & G3 . 0 = q2' & G3 . 1 = p2' ) by A80, A81; :: thesis:

end;

then consider G3 being Path of q2',p2' such that
A82: ( G3 is continuous & G3 . 0 = q2' & G3 . 1 = p2' ) ;
( (G1 + G2) + G3 is continuous & ((G1 + G2) + G3) . 0 = p1' & ((G1 + G2) + G3) . 1 = p2' ) by A63, A82, BORSUK_2:17;
hence contradiction by A1, A2, A7, A21, Th18; :: thesis:

end;

case q in Segment P,p1,p2,q2,p2 ; :: thesis:

then q in { p3 where p3 is Point of (TOP-REAL 2) : ( LE q2,p3,P,p1,p2 & LE p3,p2,P,p1,p2 ) } by JORDAN6:29;
then consider p3 being Point of (TOP-REAL 2) such that
A83: ( q = p3 & LE q2,p3,P,p1,p2 & LE p3,p2,P,p1,p2 ) ;
not q1 in {q2} by A5, TARSKI:def 1;
then reconsider Qa = P \ {q2} as non empty Subset of ((TOP-REAL 2) | P) by A2, A15, XBOOLE_0:def 5, XBOOLE_1:36;
reconsider Qa' = Qa as Subset of (TOP-REAL 2) ;

A84: now

assume A85: p2 = q2 ; :: thesis:
then q = p2 by A1, A83, JORDAN5C:12;
hence contradiction by A6, A11, A85, TOPREAL1:4; :: thesis:

end;

A86: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:29;
A87: not p2 in {q2} by A84, TARSKI:def 1;
A88: not p1 in {q2} by A9, TARSKI:def 1;
A89: not q1 in {q2} by A5, TARSKI:def 1;
not q in {q2} by A11, A12, TARSKI:def 1;
then reconsider p1' = p1, q' = q, q1' = q1, p2' = p2 as Point of (((TOP-REAL 2) | P) | Qa) by A1, A2, A4, A11, A86, A87, A88, A89, XBOOLE_0:def 5;

now

per cases ;

case q <> p2 ; :: thesis:

then A90: Segment P,p1,p2,q,p2 is_an_arc_of q,p2 by A1, A11, Th22;
then consider f1 being Function of I[01] ,((TOP-REAL 2) | (Segment P,p1,p2,q,p2)) such that
A91: ( f1 is being_homeomorphism & f1 . 0 = q & f1 . 1 = p2 ) by TOPREAL1:def 2;
A92: f1 is continuous by A91, TOPS_2:def 5;
A93: dom f1 = the carrier of I[01] by A14, A91, TOPS_2:def 5;
A94: rng f1 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,q,p2)) by A91, TOPS_2:def 5
.= Segment P,p1,p2,q,p2 by PRE_TOPC:def 10 ;
{ p where p is Point of (TOP-REAL 2) : ( LE q,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } c= Qa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( LE q,p,P,p1,p2 & LE p,p2,P,p1,p2 ) } ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A95: ( x = p & LE q,p,P,p1,p2 & LE p,p2,P,p1,p2 ) ;
x <> q2 by A1, A11, A12, A83, A95, JORDAN5C:12;
then ( x in P & not x in {q2} ) by A95, JORDAN5C:def 3, TARSKI:def 1;
hence x in Qa by XBOOLE_0:def 5; :: thesis:

end;

then A96: Segment P,p1,p2,q,p2 c= Qa by JORDAN6:29;
then reconsider g1 = f1 as Function of I[01] ,(((TOP-REAL 2) | P) | Qa) by A86, A93, A94, FUNCT_2:4;
A97: [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g1 " G is open

proof

let G be Subset of (((TOP-REAL 2) | P) | Qa); :: thesis:
assume A98: G is open ; :: thesis:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa' by PRE_TOPC:28, XBOOLE_1:36;
then consider G4 being Subset of (TOP-REAL 2) such that
A99: ( G4 is open & G = G4 /\ ([#] ((TOP-REAL 2) | Qa')) ) by A98, TOPS_2:32;
reconsider G5 = G4 /\ ([#] ((TOP-REAL 2) | (Segment P,p1,p2,q,p2))) as Subset of ((TOP-REAL 2) | (Segment P,p1,p2,q,p2)) ;
p2 in Segment P,p1,p2,q,p2 by A90, TOPREAL1:4;
then A100: not [#] ((TOP-REAL 2) | (Segment P,p1,p2,q,p2)) is empty ;
A101: G5 is open by A99, TOPS_2:32;
A102: f1 " G5 = g1 " (G4 /\ (Segment P,p1,p2,q,p2)) by PRE_TOPC:def 10
.= (g1 " G4) /\ (g1 " (Segment P,p1,p2,q,p2)) by FUNCT_1:137 ;
A103: rng g1 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,q,p2)) by A91, TOPS_2:def 5
.= Segment P,p1,p2,q,p2 by PRE_TOPC:def 10 ;
g1 " G = (g1 " G4) /\ (g1 " ([#] ((TOP-REAL 2) | Qa'))) by A99, FUNCT_1:137
.= (g1 " G4) /\ (g1 " Qa') by PRE_TOPC:def 10
.= (g1 " G4) /\ (g1 " ((rng g1) /\ Qa')) by RELAT_1:168
.= (g1 " G4) /\ (g1 " (Segment P,p1,p2,q,p2)) by A96, A103, XBOOLE_1:28 ;
hence g1 " G is open by A92, A100, A101, A102, TOPS_2:55; :: thesis:

end;

then A104: g1 is continuous by A97, TOPS_2:55;
then q',p2' are_connected by A91, BORSUK_2:def 1;
then g1 is Path of q',p2' by A91, A104, BORSUK_2:def 2;
hence ex G1 being Path of q',p2' st
( G1 is continuous & G1 . 0 = q' & G1 . 1 = p2' ) by A91, A104; :: thesis:

end;

case A105: q = p2 ; :: thesis:

consider g01 being Function of I[01] ,(((TOP-REAL 2) | P) | Qa) such that
A106: ( g01 is continuous & g01 . 0 = p2' & g01 . 1 = p2' ) by BORSUK_2:4;
p2',p2' are_connected ;
then g01 is Path of p2',p2' by A106, BORSUK_2:def 2;
hence ex G1 being Path of q',p2' st
( G1 is continuous & G1 . 0 = q' & G1 . 1 = p2' ) by A105, A106; :: thesis:

end;

then consider G1 being Path of q',p2' such that
A107: ( G1 is continuous & G1 . 0 = q' & G1 . 1 = p2' ) ;
A108: Segment Q1,q1,q2,q1,q is_an_arc_of q1,q by A1, A11, A13, JORDAN16:39;
then consider f2 being Function of I[01] ,((TOP-REAL 2) | (Segment Q1,q1,q2,q1,q)) such that
A109: ( f2 is being_homeomorphism & f2 . 0 = q1 & f2 . 1 = q ) by TOPREAL1:def 2;
A110: f2 is continuous by A109, TOPS_2:def 5;
A111: dom f2 = the carrier of I[01] by A14, A109, TOPS_2:def 5;
A112: rng f2 = [#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q1,q)) by A109, TOPS_2:def 5
.= Segment Q1,q1,q2,q1,q by PRE_TOPC:def 10 ;
A113: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:29;
{ p where p is Point of (TOP-REAL 2) : ( LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) } c= Qa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) } ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A114: ( x = p & LE q1,p,Q1,q1,q2 & LE p,q,Q1,q1,q2 ) ;
A115: x in Q1 by A114, JORDAN5C:def 3;

now

assume A116: x = q2 ; :: thesis:
LE q,q2,Q1,q1,q2 by A1, A11, JORDAN5C:10;
hence contradiction by A1, A11, A12, A114, A116, JORDAN5C:12; :: thesis:

end;

then ( x in P & not x in {q2} ) by A1, A115, TARSKI:def 1;
hence x in Qa by XBOOLE_0:def 5; :: thesis:

end;

then A117: Segment Q1,q1,q2,q1,q c= Qa by JORDAN6:29;
then reconsider g2 = f2 as Function of I[01] ,(((TOP-REAL 2) | P) | Qa) by A111, A112, A113, FUNCT_2:4;
A118: [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g2 " G is open

proof

let G be Subset of (((TOP-REAL 2) | P) | Qa); :: thesis:
assume A119: G is open ; :: thesis:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa' by PRE_TOPC:28, XBOOLE_1:36;
then consider G4 being Subset of (TOP-REAL 2) such that
A120: ( G4 is open & G = G4 /\ ([#] ((TOP-REAL 2) | Qa')) ) by A119, TOPS_2:32;
reconsider G5 = G4 /\ ([#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q1,q))) as Subset of ((TOP-REAL 2) | (Segment Q1,q1,q2,q1,q)) ;
q1 in Segment Q1,q1,q2,q1,q by A108, TOPREAL1:4;
then A121: not [#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q1,q)) is empty ;
A122: G5 is open by A120, TOPS_2:32;
A123: f2 " G5 = g2 " (G4 /\ (Segment Q1,q1,q2,q1,q)) by PRE_TOPC:def 10
.= (g2 " G4) /\ (g2 " (Segment Q1,q1,q2,q1,q)) by FUNCT_1:137 ;
A124: rng g2 = [#] ((TOP-REAL 2) | (Segment Q1,q1,q2,q1,q)) by A109, TOPS_2:def 5
.= Segment Q1,q1,q2,q1,q by PRE_TOPC:def 10 ;
g2 " G = (g2 " G4) /\ (g2 " ([#] ((TOP-REAL 2) | Qa'))) by A120, FUNCT_1:137
.= (g2 " G4) /\ (g2 " Qa') by PRE_TOPC:def 10
.= (g2 " G4) /\ (g2 " ((rng g2) /\ Qa')) by RELAT_1:168
.= (g2 " G4) /\ (g2 " (Segment Q1,q1,q2,q1,q)) by A117, A124, XBOOLE_1:28 ;
hence g2 " G is open by A110, A121, A122, A123, TOPS_2:55; :: thesis:

end;

then A125: g2 is continuous by A118, TOPS_2:55;
then q1',q' are_connected by A109, BORSUK_2:def 1;
then reconsider G2 = g2 as Path of q1',q' by A109, A125, BORSUK_2:def 2;
A126: ( G2 + G1 is continuous & (G2 + G1) . 0 = q1' & (G2 + G1) . 1 = p2' ) by A107, A109, A125, BORSUK_2:17;

now

per cases ;

case q1 <> p1 ; :: thesis:

then A127: Segment P,p1,p2,p1,q1 is_an_arc_of p1,q1 by A1, A2, JORDAN16:39;
then consider f3 being Function of I[01] ,((TOP-REAL 2) | (Segment P,p1,p2,p1,q1)) such that
A128: ( f3 is being_homeomorphism & f3 . 0 = p1 & f3 . 1 = q1 ) by TOPREAL1:def 2;
A129: f3 is continuous by A128, TOPS_2:def 5;
A130: dom f3 = the carrier of I[01] by A14, A128, TOPS_2:def 5;
A131: rng f3 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q1)) by A128, TOPS_2:def 5
.= Segment P,p1,p2,p1,q1 by PRE_TOPC:def 10 ;
A132: the carrier of (((TOP-REAL 2) | P) | Qa) = Qa by PRE_TOPC:29;
{ p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2 ) } c= Qa

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Point of (TOP-REAL 2) : ( LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2 ) } ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A133: ( x = p & LE p1,p,P,p1,p2 & LE p,q1,P,p1,p2 ) ;
x <> q2 by A1, A133, JORDAN5C:12, JORDAN6:49;
then ( x in P & not x in {q2} ) by A133, JORDAN5C:def 3, TARSKI:def 1;
hence x in Qa by XBOOLE_0:def 5; :: thesis:

end;

then A134: Segment P,p1,p2,p1,q1 c= Qa by JORDAN6:29;
then reconsider g3 = f3 as Function of I[01] ,(((TOP-REAL 2) | P) | Qa) by A130, A131, A132, FUNCT_2:4;
A135: [#] (((TOP-REAL 2) | P) | Qa) <> {} ;
for G being Subset of (((TOP-REAL 2) | P) | Qa) st G is open holds
g3 " G is open

proof

let G be Subset of (((TOP-REAL 2) | P) | Qa); :: thesis:
assume A136: G is open ; :: thesis:
((TOP-REAL 2) | P) | Qa = (TOP-REAL 2) | Qa' by PRE_TOPC:28, XBOOLE_1:36;
then consider G4 being Subset of (TOP-REAL 2) such that
A137: ( G4 is open & G = G4 /\ ([#] ((TOP-REAL 2) | Qa')) ) by A136, TOPS_2:32;
reconsider G5 = G4 /\ ([#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q1))) as Subset of ((TOP-REAL 2) | (Segment P,p1,p2,p1,q1)) ;
p1 in Segment P,p1,p2,p1,q1 by A127, TOPREAL1:4;
then A138: not [#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q1)) is empty ;
A139: G5 is open by A137, TOPS_2:32;
A140: f3 " G5 = g3 " (G4 /\ (Segment P,p1,p2,p1,q1)) by PRE_TOPC:def 10
.= (g3 " G4) /\ (g3 " (Segment P,p1,p2,p1,q1)) by FUNCT_1:137 ;
A141: rng g3 = [#] ((TOP-REAL 2) | (Segment P,p1,p2,p1,q1)) by A128, TOPS_2:def 5
.= Segment P,p1,p2,p1,q1 by PRE_TOPC:def 10 ;
g3 " G = (g3 " G4) /\ (g3 " ([#] ((TOP-REAL 2) | Qa'))) by A137, FUNCT_1:137
.= (g3 " G4) /\ (g3 " Qa') by PRE_TOPC:def 10
.= (g3 " G4) /\ (g3 " ((rng g3) /\ Qa')) by RELAT_1:168
.= (g3 " G4) /\ (g3 " (Segment P,p1,p2,p1,q1)) by A134, A141, XBOOLE_1:28 ;
hence g3 " G is open by A129, A138, A139, A140, TOPS_2:55; :: thesis:

end;

then A142: g3 is continuous by A135, TOPS_2:55;
then p1',q1' are_connected by A128, BORSUK_2:def 1;
then g3 is Path of p1',q1' by A128, A142, BORSUK_2:def 2;
hence ex G3 being Path of p1',q1' st
( G3 is continuous & G3 . 0 = p1' & G3 . 1 = q1' ) by A128, A142; :: thesis:

end;

case A143: q1 = p1 ; :: thesis:

consider g01 being Function of I[01] ,(((TOP-REAL 2) | P) | Qa) such that
A144: ( g01 is continuous & g01 . 0 = q1' & g01 . 1 = q1' ) by BORSUK_2:4;
q1',q1' are_connected ;
then g01 is Path of q1',q1' by A144, BORSUK_2:def 2;
hence ex G3 being Path of p1',q1' st
( G3 is continuous & G3 . 0 = p1' & G3 . 1 = q1' ) by A143, A144; :: thesis:

end;

then consider G3 being Path of p1',q1' such that
A145: ( G3 is continuous & G3 . 0 = p1' & G3 . 1 = q1' ) ;
( G3 + (G2 + G1) is continuous & (G3 + (G2 + G1)) . 0 = p1' & (G3 + (G2 + G1)) . 1 = p2' ) by A126, A145, BORSUK_2:17;
hence contradiction by A1, A3, A9, A84, Th18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence Q1 = Segment P,p1,p2,q1,q2 by A1, A6, Th21; :: thesis: