let n be Element of NAT ; :: thesis: the_Complex_Space n is regular
let p be Point of (the_Complex_Space n); :: according to COMPTS_1:def 5 :: thesis: for b₁ being Element of K10(the carrier of (the_Complex_Space n)) holds
( b₁ = {} or not b₁ is closed or not p in b₁ ` or ex b<sub>2</sub>, b<sub>3</sub> being Element of K10(the carrier of (the_Complex_Space n)) st
( b<sub>2</sub> is open & b<sub>3</sub> is open & p in b<sub>2</sub> & b<sub>1</sub> c= b<sub>3</sub> & b<sub>2</sub> misses b<sub>3</sub> ) )
let P be Subset of (the_Complex_Space n); :: thesis: ( P = {} or not P is closed or not p in P ` or ex b₁, b₂ being Element of K10(the carrier of (the_Complex_Space n)) st
( b₁ is open & b₂ is open & p in b₁ & P c= b₂ & b₁ misses b₂ ) )
assume that
A1: P <> {} and
A2: ( P is closed & p in P ` ) ; :: thesis: ex b₁, b₂ being Element of K10(the carrier of (the_Complex_Space n)) st
( b₁ is open & b₂ is open & p in b₁ & P c= b₂ & b₁ misses b₂ )
reconsider A = P as Subset of (COMPLEX n) ;
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 (the_Complex_Space n) ;
take K1 ; :: thesis: ex b₁ being Element of K10(the carrier of (the_Complex_Space n)) st
( K1 is open & b₁ is open & p in K1 & P c= b₁ & K1 misses b₁ )
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:129;
Ball A,((dist z1,A) / 2) is open by A1, SEQ_4:139;
hence ( K1 is open & K2 is open ) by A3, Th108; :: thesis: ( p in K1 & P c= K2 & K1 misses K2 )
( A is closed & not p in P ) by A2, Th110, XBOOLE_0:def 5;
then 0 < (dist z1,A) / 2 by A1, SEQ_4:134, XREAL_1:217;
hence ( p in K1 & P c= K2 ) by SEQ_4:128, SEQ_4:138; :: 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:10;
x in K2 by A4, XBOOLE_0:def 4;
then A5: dist x,A < (dist z1,A) / 2 by SEQ_4:136;
x in K1 by A4, XBOOLE_0:def 4;
then |.(z1 - x).| < (dist z1,A) / 2 by SEQ_4:127;
then |.(z1 - x).| + (dist x,A) < ((dist z1,A) / 2) + ((dist z1,A) / 2) by A5, XREAL_1:10;
hence contradiction by A1, SEQ_4:135; :: thesis: verum