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_of (TOP-REAL 2) | (C ` ) & V is_a_component_of (TOP-REAL 2) | (C ` ) & 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_of (TOP-REAL 2) | (C ` ) & V is_a_component_of (TOP-REAL 2) | (C ` ) & U <> V holds
Cl P misses V
let U, V be Subset of ((TOP-REAL 2) | (C ` )); :: thesis: ( U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) & V is_a_component_of (TOP-REAL 2) | (C ` ) & U <> V implies Cl P misses V )
assume that
A1: U = P and
A2: U is_a_component_of (TOP-REAL 2) | (C ` ) and
A3: V is_a_component_of (TOP-REAL 2) | (C ` ) and
A4: U <> V ; :: thesis: Cl P misses V
assume Cl P meets V ; :: thesis: contradiction
then A5: ex x being set st
( x in Cl P & x in V ) by XBOOLE_0:3;
the carrier of ((TOP-REAL 2) | (C ` )) = C ` by PRE_TOPC:29;
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:89;
then V is open by A3, CONNSP_2:21;
then V1 is open by TSEP_1:17;
then P meets V1 by A5, PRE_TOPC:def 13;
hence contradiction by A1, A2, A3, A4, CONNSP_1:37; :: thesis: verum