let n be Element of NAT ; :: thesis:
let p be Point of ; :: according to COMPTS_1:def 2 :: thesis: for b1 being Element of K10( the carrier of ) holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of K10( the carrier of ) st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )

let P be Subset of ; :: thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of K10( the carrier of ) st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )

assume that
A1: P <> {} and
A2: ( P is closed & p in P ` ) ; :: thesis: ex b1, b2 being Element of K10( the carrier of ) st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )

reconsider A = P as Subset of () ;
reconsider z1 = p as Element of COMPLEX n ;
set d = (dist (z1,A)) / 2;
reconsider K1 = Ball (z1,((dist (z1,A)) / 2)), K2 = Ball (A,((dist (z1,A)) / 2)) as Subset of ;
take K1 ; :: thesis: ex b1 being Element of K10( the carrier of ) st
( K1 is open & b1 is open & p in K1 & P c= b1 & K1 misses b1 )

take K2 ; :: thesis: ( K1 is open & K2 is open & p in K1 & P c= K2 & K1 misses K2 )
A3: Ball (z1,((dist (z1,A)) / 2)) is open by SEQ_4:112;
Ball (A,((dist (z1,A)) / 2)) is open by ;
hence ( K1 is open & K2 is open ) by A3; :: thesis: ( p in K1 & P c= K2 & K1 misses K2 )
( A is closed & not p in P ) by ;
then 0 < (dist (z1,A)) / 2 by ;
hence ( p in K1 & P c= K2 ) by ; :: thesis: K1 misses K2
assume K1 /\ K2 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being Element of COMPLEX n such that
A4: x in (Ball (z1,((dist (z1,A)) / 2))) /\ (Ball (A,((dist (z1,A)) / 2))) by SUBSET_1:4;
x in K2 by ;
then A5: dist (x,A) < (dist (z1,A)) / 2 by SEQ_4:119;
x in K1 by ;
then |.(z1 - x).| < (dist (z1,A)) / 2 by SEQ_4:110;
then |.(z1 - x).| + (dist (x,A)) < ((dist (z1,A)) / 2) + ((dist (z1,A)) / 2) by ;
hence contradiction by A1, SEQ_4:118; :: thesis: verum