let n be Nat; :: thesis: for P, P1, P2 being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

let P, P1, P2 be Subset of (TOP-REAL n); :: thesis: for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

let Q be Subset of ((TOP-REAL n) | P); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} implies Q is open )

assume that

A1: P2 is_an_arc_of p1,p2 and

A2: P1 \/ P2 = P and

A3: P1 /\ P2 = {p1,p2} and

A4: Q = P1 \ {p1,p2} ; :: thesis: Q is open

reconsider P21 = P2 as Subset of (TOP-REAL n) ;

A5: P21 is compact by A1, JORDAN5A:1;

p1 in P1 /\ P2 by A3, TARSKI:def 2;

then A6: p1 in P2 by XBOOLE_0:def 4;

A7: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

then reconsider P29 = P21 as Subset of ((TOP-REAL n) | P) by A2, XBOOLE_1:7;

p2 in P1 /\ P2 by A3, TARSKI:def 2;

then A8: p2 in P2 by XBOOLE_0:def 4;

P29 is compact by A5, A7, COMPTS_1:2;

then A9: P29 is closed by COMPTS_1:7;

A10: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by A2, XBOOLE_1:42

.= (P1 \ P2) \/ {} by XBOOLE_1:37

.= P1 \ P2 ;

A11: P1 \ P2 c= Q

then Q = P29 ` by A7, A10, SUBSET_1:def 4;

hence Q is open by A9, TOPS_1:3; :: thesis: verum

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

let P, P1, P2 be Subset of (TOP-REAL n); :: thesis: for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

let Q be Subset of ((TOP-REAL n) | P); :: thesis: for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

let p1, p2 be Point of (TOP-REAL n); :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} implies Q is open )

assume that

A1: P2 is_an_arc_of p1,p2 and

A2: P1 \/ P2 = P and

A3: P1 /\ P2 = {p1,p2} and

A4: Q = P1 \ {p1,p2} ; :: thesis: Q is open

reconsider P21 = P2 as Subset of (TOP-REAL n) ;

A5: P21 is compact by A1, JORDAN5A:1;

p1 in P1 /\ P2 by A3, TARSKI:def 2;

then A6: p1 in P2 by XBOOLE_0:def 4;

A7: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

then reconsider P29 = P21 as Subset of ((TOP-REAL n) | P) by A2, XBOOLE_1:7;

p2 in P1 /\ P2 by A3, TARSKI:def 2;

then A8: p2 in P2 by XBOOLE_0:def 4;

P29 is compact by A5, A7, COMPTS_1:2;

then A9: P29 is closed by COMPTS_1:7;

A10: P \ P2 = (P1 \ P2) \/ (P2 \ P2) by A2, XBOOLE_1:42

.= (P1 \ P2) \/ {} by XBOOLE_1:37

.= P1 \ P2 ;

A11: P1 \ P2 c= Q

proof

Q c= P1 \ P2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 \ P2 or x in Q )

assume A12: x in P1 \ P2 ; :: thesis: x in Q

then A13: x in P1 by XBOOLE_0:def 5;

not x in P2 by A12, XBOOLE_0:def 5;

then not x in {p1,p2} by A6, A8, TARSKI:def 2;

hence x in Q by A4, A13, XBOOLE_0:def 5; :: thesis: verum

end;assume A12: x in P1 \ P2 ; :: thesis: x in Q

then A13: x in P1 by XBOOLE_0:def 5;

not x in P2 by A12, XBOOLE_0:def 5;

then not x in {p1,p2} by A6, A8, TARSKI:def 2;

hence x in Q by A4, A13, XBOOLE_0:def 5; :: thesis: verum

proof

then
P1 \ P2 = Q
by A11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q or x in P1 \ P2 )

assume A14: x in Q ; :: thesis: x in P1 \ P2

then A15: x in P1 by A4, XBOOLE_0:def 5;

not x in {p1,p2} by A4, A14, XBOOLE_0:def 5;

then not x in P2 by A3, A15, XBOOLE_0:def 4;

hence x in P1 \ P2 by A15, XBOOLE_0:def 5; :: thesis: verum

end;assume A14: x in Q ; :: thesis: x in P1 \ P2

then A15: x in P1 by A4, XBOOLE_0:def 5;

not x in {p1,p2} by A4, A14, XBOOLE_0:def 5;

then not x in P2 by A3, A15, XBOOLE_0:def 4;

hence x in P1 \ P2 by A15, XBOOLE_0:def 5; :: thesis: verum

then Q = P29 ` by A7, A10, SUBSET_1:def 4;

hence Q is open by A9, TOPS_1:3; :: thesis: verum