let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2)
for U, V being Subset of ((TOP-REAL 2) | (C `)) st U = P & U is a_component & V is a_component & U <> V holds
Cl P misses V
let P be Subset of (TOP-REAL 2); :: thesis: for U, V being Subset of ((TOP-REAL 2) | (C `)) st U = P & U is a_component & V is a_component & U <> V holds
Cl P misses V
let U, V be Subset of ((TOP-REAL 2) | (C `)); :: thesis: ( U = P & U is a_component & V is a_component & U <> V implies Cl P misses V )
assume that
A1: U = P and
A2: U is a_component and
A3: V is a_component and
A4: U <> V ; :: thesis: Cl P misses V
assume Cl P meets V ; :: thesis: contradiction
then A5: ex x being object st
( x in Cl P & x in V ) by XBOOLE_0:3;
the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
then reconsider V1 = V as Subset of (TOP-REAL 2) by XBOOLE_1:1;
reconsider T2C = (TOP-REAL 2) | (C `) as non empty SubSpace of TOP-REAL 2 ;
T2C is locally_connected by JORDAN2C:81;
then V is open by A3, CONNSP_2:15;
then V1 is open by TSEP_1:17;
then P meets V1 by A5, PRE_TOPC:def 7;
hence contradiction by A1, A2, A3, A4, CONNSP_1:35; :: thesis: verum