let n be Element of NAT ; the_Complex_Space n is T_2
let p be Point of (the_Complex_Space n); PRE_TOPC:def 10 for b1 being Element of the carrier of (the_Complex_Space n) holds
( p = b1 or ex b2, b3 being Element of K10( the carrier of (the_Complex_Space n)) st
( b2 is open & b3 is open & p in b2 & b1 in b3 & b2 misses b3 ) )
let q be Point of (the_Complex_Space n); ( p = q or ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A1:
p <> q
; ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
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
; ex b1 being Element of K10( the carrier of (the_Complex_Space n)) st
( K1 is open & b1 is open & p in K1 & q in b1 & K1 misses b1 )
take
K2
; ( 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 )
; ( 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; K1 misses K2
assume
K1 /\ K2 <> {}
; XBOOLE_0:def 7 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; verum