let P be Subset of ; :: thesis: for Q being Subset of
for p1, p2 being Point of 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 ; :: thesis: for p1, p2 being Point of 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 ; :: 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 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 10;
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 P1' = P1 \ {p1,p2} as Subset of 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 P2' = P2 \ {p1,p2} as Subset of by A10, A12, XBOOLE_1:1;
A13: P1' is open by A7, A8, A9, Th52;
A14: P2' is open by A6, A8, A9, Th52;
A15: 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 A16: x in Q ; :: thesis: x in P1' \/ P2'
then A17: x in P by A5, 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 A5, A8, A16, A17, XBOOLE_0:def 3, XBOOLE_0:def 5;

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 such that
A18: p3 in P1 and
A19: p3 <> p1 and
A20: p3 <> p2 by A6, Th55;
not p3 in {p1,p2} by A19, A20, TARSKI:def 2;
then A21: P1' <> {} by A18, 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 A22: x in P1' ; :: 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 P1' /\ Q <> {} by A21, XBOOLE_1:28;
then A25: P1' meets Q by XBOOLE_0:def 7;
consider p3' being Point of such that
A26: p3' in P2 and
A27: p3' <> p1 and
A28: p3' <> p2 by A7, Th55;
not p3' in {p1,p2} by A27, A28, TARSKI:def 2;
then A29: P2' <> {} by A26, 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 A30: x in P2' ; :: 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 P2' /\ Q <> {} by A29, XBOOLE_1:28;
then A33: P2' meets Q by XBOOLE_0:def 7;

now

assume P1' meets P2' ; :: thesis: contradiction
then consider p0 being set such that
A34: p0 in P1' and
A35: p0 in P2' 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:4; :: thesis: verum