let P be Subset of (TOP-REAL 2); :: thesis: for Q being Subset of ((TOP-REAL 2) | P)
for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds
not Q is connected
let Q be Subset of ((TOP-REAL 2) | P); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds
not Q is connected
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} implies not Q is connected )
assume that
A1: P is being_simple_closed_curve and
A2: p1 in P and
A3: p2 in P and
A4: p1 <> p2 and
A5: Q = P \ {p1,p2} ; :: thesis: not Q is connected
consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A6: P1 is_an_arc_of p1,p2 and
A7: P2 is_an_arc_of p1,p2 and
A8: P = P1 \/ P2 and
A9: P1 /\ P2 = {p1,p2} by A1, A2, A3, A4, TOPREAL2:5;
A10: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 5;
reconsider P = P as Simple_closed_curve by A1;
A11: P1 c= P by A8, XBOOLE_1:7;
P1 \ {p1,p2} c= P1 by XBOOLE_1:36;
then reconsider P19 = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A10, A11, XBOOLE_1:1;
A12: P2 c= P by A8, XBOOLE_1:7;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider P29 = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A10, A12, XBOOLE_1:1;
A13: P19 is open by A7, A8, A9, Th39;
A14: P29 is open by A6, A8, A9, Th39;
A15: Q c= P19 \/ P29

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in P19 \/ P29 )
assume A16: x in Q ; :: thesis: x in P19 \/ P29
then A17: x in P by A5, XBOOLE_0:def 5;

now :: thesis: ( ( x in P1 & not x in {p1,p2} & x in P19 \/ P29 ) or ( x in P2 & not x in {p1,p2} & x in P19 \/ P29 ) )

per cases ( ( x in P1 & not x in {p1,p2} ) or ( x in P2 & not x in {p1,p2} ) ) by A5, A8, A16, A17, XBOOLE_0:def 3, XBOOLE_0:def 5;

case ( x in P1 & not x in {p1,p2} ) ; :: thesis: x in P19 \/ P29

then x in P19 by XBOOLE_0:def 5;
hence x in P19 \/ P29 by XBOOLE_0:def 3; :: thesis: verum

end;

case ( x in P2 & not x in {p1,p2} ) ; :: thesis: x in P19 \/ P29

then x in P29 by XBOOLE_0:def 5;
hence x in P19 \/ P29 by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

end;

consider p3 being Point of (TOP-REAL 2) such that
A18: p3 in P1 and
A19: p3 <> p1 and
A20: p3 <> p2 by A6, Th42;
not p3 in {p1,p2} by A19, A20, TARSKI:def 2;
then A21: P19 <> {} by A18, XBOOLE_0:def 5;
P19 c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P19 or x in Q )
assume A22: x in P19 ; :: thesis: x in Q
then A23: x in P1 by XBOOLE_0:def 5;
A24: not x in {p1,p2} by A22, XBOOLE_0:def 5;
x in P by A8, A23, XBOOLE_0:def 3;
hence x in Q by A5, A24, XBOOLE_0:def 5; :: thesis: verum

end;

then P19 /\ Q <> {} by A21, XBOOLE_1:28;
then A25: P19 meets Q ;
consider p39 being Point of (TOP-REAL 2) such that
A26: p39 in P2 and
A27: p39 <> p1 and
A28: p39 <> p2 by A7, Th42;
not p39 in {p1,p2} by A27, A28, TARSKI:def 2;
then A29: P29 <> {} by A26, XBOOLE_0:def 5;
P29 c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P29 or x in Q )
assume A30: x in P29 ; :: thesis: x in Q
then A31: x in P2 by XBOOLE_0:def 5;
A32: not x in {p1,p2} by A30, XBOOLE_0:def 5;
x in P1 \/ P2 by A31, XBOOLE_0:def 3;
hence x in Q by A5, A8, A32, XBOOLE_0:def 5; :: thesis: verum

end;

then P29 /\ Q <> {} by A29, XBOOLE_1:28;
then A33: P29 meets Q ;

now :: thesis: not P19 meets P29

assume P19 meets P29 ; :: thesis: contradiction
then consider p0 being object such that
A34: p0 in P19 and
A35: p0 in P29 by XBOOLE_0:3;
A36: p0 in P1 by A34, XBOOLE_0:def 5;
A37: not p0 in {p1,p2} by A34, XBOOLE_0:def 5;
p0 in P2 by A35, XBOOLE_0:def 5;
hence contradiction by A9, A36, A37, XBOOLE_0:def 4; :: thesis: verum

end;

hence not Q is connected by A13, A14, A15, A25, A33, TOPREAL5:1; :: thesis: verum