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

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 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 A33: P29 meets Q ;

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

consider p3 being Point of (TOP-REAL 2) such that
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;

end;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 ) )

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

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

then
P19 /\ Q <> {}
by A21, XBOOLE_1:28;
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;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

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

then
P29 /\ Q <> {}
by A29, XBOOLE_1:28;
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;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

then A33: P29 meets Q ;

now :: thesis: not P19 meets P29

hence
not Q is connected
by A13, A14, A15, A25, A33, TOPREAL5:1; :: thesis: verumassume
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;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