let p be Point of (TOP-REAL 2); :: thesis: for C being Simple_closed_curve
for U being Subset of ((TOP-REAL 2) | (C `)) st p in C holds
{p} misses U
let C be Simple_closed_curve; :: thesis: for U being Subset of ((TOP-REAL 2) | (C `)) st p in C holds
{p} misses U
let U be Subset of ((TOP-REAL 2) | (C `)); :: thesis: ( p in C implies {p} misses U )
assume A1: p in C ; :: thesis: {p} misses U
A2: U is Subset of (TOP-REAL 2) by PRE_TOPC:11;
the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
then U misses C by A2, SUBSET_1:23;
then not p in U by A1, XBOOLE_0:3;
hence {p} misses U by ZFMISC_1:50; :: thesis: verum