let P be Subset of (); :: thesis: for Q being Subset of (() | P)
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 (() | P); :: 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 ;
A10: [#] (() | P) = P by PRE_TOPC:def 5;
reconsider P = P as Simple_closed_curve by A1;
A11: P1 c= P by ;
P1 \ {p1,p2} c= P1 by XBOOLE_1:36;
then reconsider P19 = P1 \ {p1,p2} as Subset of (() | P) by ;
A12: P2 c= P by ;
P2 \ {p1,p2} c= P2 by XBOOLE_1:36;
then reconsider P29 = P2 \ {p1,p2} as Subset of (() | P) by ;
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 ;
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 ;
case ( x in P1 & not x in {p1,p2} ) ; :: thesis: x in P19 \/ P29
end;
case ( x in P2 & not x in {p1,p2} ) ; :: thesis: x in P19 \/ P29
end;
end;
end;
hence x in P19 \/ P29 ; :: thesis: verum
end;
consider p3 being Point of () such that
A18: p3 in P1 and
A19: p3 <> p1 and
A20: p3 <> p2 by ;
not p3 in {p1,p2} by ;
then A21: P19 <> {} by ;
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 ;
x in P by ;
hence x in Q by ; :: thesis: verum
end;
then P19 /\ Q <> {} by ;
then A25: P19 meets Q ;
consider p39 being Point of () such that
A26: p39 in P2 and
A27: p39 <> p1 and
A28: p39 <> p2 by ;
not p39 in {p1,p2} by ;
then A29: P29 <> {} by ;
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 ;
x in P1 \/ P2 by ;
hence x in Q by ; :: thesis: verum
end;
then P29 /\ Q <> {} by ;
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 ;
A37: not p0 in {p1,p2} by ;
p0 in P2 by ;
hence contradiction by A9, A36, A37, XBOOLE_0:def 4; :: thesis: verum
end;
hence not Q is connected by ; :: thesis: verum