let P be non empty Subset of (TOP-REAL 2); :: thesis:
let Q be Subset of ((TOP-REAL 2) | P); :: thesis:
let p1, p2, q be Point of (TOP-REAL 2); :: thesis:
assume that
A1: P is_an_arc_of p1,p2 and
A2: q in P and
A3: q <> p1 and
A4: q <> p2 and
A5: Q = P \ {q} ; :: thesis:
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A6: f is being_homeomorphism and
A7: f . 0 = p1 and
A8: f . 1 = p2 by A1, TOPREAL1:def 1;
A9: rng f = [#] ((TOP-REAL 2) | P) by A6, TOPS_2:def 5;
A10: [#] I[01] = [.0,1.] by TOPMETR:18, TOPMETR:20;
A11: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;
then consider xs being object such that
A12: xs in dom f and
A13: f . xs = q by A2, A9, FUNCT_1:def 3;
A14: dom f = [#] I[01] by A6, TOPS_2:def 5;
reconsider s = xs as Real by A12;
{ q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } c= the carrier of ((TOP-REAL 2) | P)

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } ; :: thesis:
then consider q0 being Point of (TOP-REAL 2) such that
A15: q0 = z and
A16: ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) ;
consider ss being Real such that
A17: s < ss and
A18: ss <= 1 and
A19: q0 = f . ss by A16;
ss > 0 by A12, A10, A17, XXREAL_1:1;
then ss in dom f by A14, A10, A18, XXREAL_1:1;
then q0 in rng f by A19, FUNCT_1:def 3;
hence z in the carrier of ((TOP-REAL 2) | P) by A15; :: thesis:

end;

then reconsider P29 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } as Subset of ((TOP-REAL 2) | P) ;
A20: 0 <= s by A12, A10, XXREAL_1:1;
then A21: P29 is open by A6, Th16;
A22: P29 c= Q

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in P29 ; :: thesis:
then consider q00 being Point of (TOP-REAL 2) such that
A23: q00 = x and
A24: ex ss being Real st
( s < ss & ss <= 1 & q00 = f . ss ) ;
consider ss being Real such that
A25: s < ss and
A26: ss <= 1 and
A27: q00 = f . ss by A24;
ss > 0 by A12, A10, A25, XXREAL_1:1;
then A28: ss in dom f by A14, A10, A26, XXREAL_1:1;

end;

end;

{ q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } c= the carrier of ((TOP-REAL 2) | P)

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } ; :: thesis:
then consider q0 being Point of (TOP-REAL 2) such that
A31: q0 = z and
A32: ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) ;
consider ss being Real such that
A33: 0 <= ss and
A34: ss < s and
A35: q0 = f . ss by A32;
s <= 1 by A12, A10, XXREAL_1:1;
then ss < 1 by A34, XXREAL_0:2;
then ss in dom f by A14, A10, A33, XXREAL_1:1;
then q0 in rng f by A35, FUNCT_1:def 3;
hence z in the carrier of ((TOP-REAL 2) | P) by A31; :: thesis:

end;

then reconsider P19 = { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( 0 <= ss & ss < s & q0 = f . ss ) } as Subset of ((TOP-REAL 2) | P) ;
A36: s <= 1 by A12, A10, XXREAL_1:1;
then A37: P19 is open by A6, Th15;
A38: Q c= P19 \/ P29

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A39: x in Q ; :: thesis:
then consider xt being object such that
A40: xt in dom f and
A41: f . xt = x by A9, FUNCT_1:def 3;
reconsider t = xt as Real by A40;
A42: t <= 1 by A10, A40, XXREAL_1:1;
reconsider qq = x as Point of (TOP-REAL 2) by A5, A39;
not x in {q} by A5, A39, XBOOLE_0:def 5;
then A43: not x = q by TARSKI:def 1;
A44: 0 <= t by A10, A40, XXREAL_1:1;

end;

end;

hence x in P19 \/ P29 ; :: thesis:

end;

assume P19 meets P29 ; :: thesis:
then consider p0 being object such that
A46: p0 in P19 and
A47: p0 in P29 by XBOOLE_0:3;
consider q00 being Point of (TOP-REAL 2) such that
A48: q00 = p0 and
A49: ex ss being Real st
( 0 <= ss & ss < s & q00 = f . ss ) by A46;
consider ss1 being Real such that
A50: 0 <= ss1 and
A51: ss1 < s and
A52: q00 = f . ss1 by A49;
ss1 < 1 by A36, A51, XXREAL_0:2;
then A53: ss1 in dom f by A14, A10, A50, XXREAL_1:1;
consider q01 being Point of (TOP-REAL 2) such that
A54: q01 = p0 and
A55: ex ss being Real st
( s < ss & ss <= 1 & q01 = f . ss ) by A47;
consider ss2 being Real such that
A56: s < ss2 and
A57: ss2 <= 1 and
A58: q01 = f . ss2 by A55;
ss2 > 0 by A12, A10, A56, XXREAL_1:1;
then A59: ss2 in dom f by A14, A10, A57, XXREAL_1:1;
f is one-to-one by A6, TOPS_2:def 5;
hence contradiction by A48, A51, A52, A54, A56, A58, A53, A59, FUNCT_1:def 4; :: thesis:

end;

1 > s by A4, A8, A13, A36, XXREAL_0:1;
then A60: p2 in { q0 where q0 is Point of (TOP-REAL 2) : ex ss being Real st
( s < ss & ss <= 1 & q0 = f . ss ) } by A8;
then reconsider Q9 = Q as non empty Subset of ((TOP-REAL 2) | P) by A22;
reconsider T = ((TOP-REAL 2) | P) | Q9 as non empty TopSpace ;
A61: the carrier of T = [#] T ;
then reconsider P299 = P29 as Subset of T by A22, PRE_TOPC:def 5;
P29 /\ Q <> {} by A60, A22, XBOOLE_1:28;
then A62: P29 meets Q by XBOOLE_0:def 7;
A63: P19 c= Q

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in P19 ; :: thesis:
then consider q00 being Point of (TOP-REAL 2) such that
A64: q00 = x and
A65: ex ss being Real st
( 0 <= ss & ss < s & q00 = f . ss ) ;
consider ss being Real such that
A66: 0 <= ss and
A67: ss < s and
A68: q00 = f . ss by A65;
ss < 1 by A36, A67, XXREAL_0:2;
then A69: ss in dom f by A14, A10, A66, XXREAL_1:1;

end;

end;