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 A1: ( P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} ) ; :: thesis: not Q is connected
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A2: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) by TOPREAL2:5;
A3: [#] ((TOP-REAL 2) | P) = P by PRE_TOPC:def 10;
reconsider P = P as Simple_closed_curve by A1;
A4: P1 c= P by A2, XBOOLE_1:7;
P1 \ {p1,p2} c= P1 by XBOOLE_1:36;
then reconsider P1' = P1 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A3, A4, XBOOLE_1:1;
A5: P2 c= P by A2, XBOOLE_1:7;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider P2' = P2 \ {p1,p2} as Subset of ((TOP-REAL 2) | P) by A3, A5, XBOOLE_1:1;
A6: P1' is open by A1, A2, Th52;
A7: P2' is open by A1, A2, Th52;
A8: Q c= P1' \/ P2'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in P1' \/ P2' )
assume x in Q ; :: thesis: x in P1' \/ P2'
then A9: ( x in P & not x in {p1,p2} ) by A1, XBOOLE_0:def 5;

now

per cases ( ( x in P1 & not x in {p1,p2} ) or ( x in P2 & not x in {p1,p2} ) ) by A2, A9, XBOOLE_0:def 3;

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

then x in P1' by XBOOLE_0:def 5;
hence x in P1' \/ P2' by XBOOLE_0:def 3; :: thesis: verum

end;

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

then x in P2' by XBOOLE_0:def 5;
hence x in P1' \/ P2' by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in P1' \/ P2' ; :: thesis: verum

end;

consider p3 being Point of (TOP-REAL 2) such that
A10: ( p3 in P1 & p3 <> p1 & p3 <> p2 ) by A2, Th55;
not p3 in {p1,p2} by A10, TARSKI:def 2;
then A11: P1' <> {} by A10, XBOOLE_0:def 5;
P1' c= Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P1' or x in Q )
assume x in P1' ; :: thesis: x in Q
then A12: ( x in P1 & not x in {p1,p2} ) by XBOOLE_0:def 5;
then x in P by A2, XBOOLE_0:def 3;
hence x in Q by A1, A12, XBOOLE_0:def 5; :: thesis: verum

end;

then P1' /\ Q <> {} by A11, XBOOLE_1:28;
then A13: P1' meets Q by XBOOLE_0:def 7;
consider p3' being Point of (TOP-REAL 2) such that
A14: ( p3' in P2 & p3' <> p1 & p3' <> p2 ) by A2, Th55;
not p3' in {p1,p2} by A14, TARSKI:def 2;
then A15: P2' <> {} by A14, XBOOLE_0:def 5;
P2' c= Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P2' or x in Q )
assume x in P2' ; :: thesis: x in Q
then A16: ( x in P2 & not x in {p1,p2} ) by XBOOLE_0:def 5;
then x in P1 \/ P2 by XBOOLE_0:def 3;
hence x in Q by A1, A2, A16, XBOOLE_0:def 5; :: thesis: verum

end;

then P2' /\ Q <> {} by A15, XBOOLE_1:28;
then A17: P2' meets Q by XBOOLE_0:def 7;

now

assume P1' meets P2' ; :: thesis: contradiction
then consider p0 being set such that
A18: ( p0 in P1' & p0 in P2' ) by XBOOLE_0:3;
A19: ( p0 in P1 & not p0 in {p1,p2} ) by A18, XBOOLE_0:def 5;
p0 in P2 by A18, XBOOLE_0:def 5;
hence contradiction by A2, A19, XBOOLE_0:def 4; :: thesis: verum

end;

hence not Q is connected by A6, A7, A8, A13, A17, TOPREAL5:4; :: thesis: verum