let P be Subset of (TOP-REAL 2); 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); 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); ( 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}
; 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
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
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
then
P29 /\ Q <> {}
by A29, XBOOLE_1:28;
then A33:
P29 meets Q
;
hence
not Q is connected
by A13, A14, A15, A25, A33, TOPREAL5:1; verum