let n be Element of NAT ; :: thesis: the_Complex_Space n is T_2

let p be Point of (the_Complex_Space n); :: according to PRE_TOPC:def 10 :: thesis: for b_{1} being Element of the carrier of (the_Complex_Space n) holds

( p = b_{1} or ex b_{2}, b_{3} being Element of K10( the carrier of (the_Complex_Space n)) st

( b_{2} is open & b_{3} is open & p in b_{2} & b_{1} in b_{3} & b_{2} misses b_{3} ) )

let q be Point of (the_Complex_Space n); :: thesis: ( p = q or ex b_{1}, b_{2} being Element of K10( the carrier of (the_Complex_Space n)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} ) )

assume A1: p <> q ; :: thesis: ex b_{1}, b_{2} being Element of K10( the carrier of (the_Complex_Space n)) st

( b_{1} is open & b_{2} is open & p in b_{1} & q in b_{2} & b_{1} misses b_{2} )

reconsider z1 = p, z2 = q as Element of COMPLEX n ;

set d = |.(z1 - z2).| / 2;

reconsider K1 = Ball (z1,(|.(z1 - z2).| / 2)), K2 = Ball (z2,(|.(z1 - z2).| / 2)) as Subset of (the_Complex_Space n) ;

take K1 ; :: thesis: ex b_{1} being Element of K10( the carrier of (the_Complex_Space n)) st

( K1 is open & b_{1} is open & p in K1 & q in b_{1} & K1 misses b_{1} )

take K2 ; :: thesis: ( K1 is open & K2 is open & p in K1 & q in K2 & K1 misses K2 )

( Ball (z1,(|.(z1 - z2).| / 2)) is open & Ball (z2,(|.(z1 - z2).| / 2)) is open ) by SEQ_4:112;

hence ( K1 is open & K2 is open ) ; :: thesis: ( p in K1 & q in K2 & K1 misses K2 )

0 < |.(z1 - z2).| by A1, SEQ_4:103;

hence ( p in K1 & q in K2 ) by SEQ_4:111, XREAL_1:215; :: 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

A2: x in (Ball (z1,(|.(z1 - z2).| / 2))) /\ (Ball (z2,(|.(z1 - z2).| / 2))) by SUBSET_1:4;

x in K2 by A2, XBOOLE_0:def 4;

then A3: |.(z2 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110;

x in K1 by A2, XBOOLE_0:def 4;

then |.(z1 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110;

then |.(z1 - x).| + |.(z2 - x).| < (|.(z1 - z2).| / 2) + (|.(z1 - z2).| / 2) by A3, XREAL_1:8;

then |.(z1 - x).| + |.(x - z2).| < |.(z1 - z2).| by SEQ_4:104;

hence contradiction by SEQ_4:105; :: thesis: verum

let p be Point of (the_Complex_Space n); :: according to PRE_TOPC:def 10 :: thesis: for b

( p = b

( b

let q be Point of (the_Complex_Space n); :: thesis: ( p = q or ex b

( b

assume A1: p <> q ; :: thesis: ex b

( b

reconsider z1 = p, z2 = q as Element of COMPLEX n ;

set d = |.(z1 - z2).| / 2;

reconsider K1 = Ball (z1,(|.(z1 - z2).| / 2)), K2 = Ball (z2,(|.(z1 - z2).| / 2)) as Subset of (the_Complex_Space n) ;

take K1 ; :: thesis: ex b

( K1 is open & b

take K2 ; :: thesis: ( K1 is open & K2 is open & p in K1 & q in K2 & K1 misses K2 )

( Ball (z1,(|.(z1 - z2).| / 2)) is open & Ball (z2,(|.(z1 - z2).| / 2)) is open ) by SEQ_4:112;

hence ( K1 is open & K2 is open ) ; :: thesis: ( p in K1 & q in K2 & K1 misses K2 )

0 < |.(z1 - z2).| by A1, SEQ_4:103;

hence ( p in K1 & q in K2 ) by SEQ_4:111, XREAL_1:215; :: 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

A2: x in (Ball (z1,(|.(z1 - z2).| / 2))) /\ (Ball (z2,(|.(z1 - z2).| / 2))) by SUBSET_1:4;

x in K2 by A2, XBOOLE_0:def 4;

then A3: |.(z2 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110;

x in K1 by A2, XBOOLE_0:def 4;

then |.(z1 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110;

then |.(z1 - x).| + |.(z2 - x).| < (|.(z1 - z2).| / 2) + (|.(z1 - z2).| / 2) by A3, XREAL_1:8;

then |.(z1 - x).| + |.(x - z2).| < |.(z1 - z2).| by SEQ_4:104;

hence contradiction by SEQ_4:105; :: thesis: verum