let n be Nat; for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
let x be Element of COMPLEX n; for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
let A be Subset of (COMPLEX n); ( A <> {} implies dist (x,A) >= 0 )
defpred S1[ set ] means $1 in A;
deffunc H1( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H2( Element of COMPLEX n) -> Real = |.(x - $1).|;
reconsider X = { H1(z) where z is Element of COMPLEX n : S1[z] } as Subset of REAL from DOMAIN_1:sch 8();
A1:
for z being Element of COMPLEX n holds H1(z) = H2(z)
;
A2:
{ H1(z1) where z1 is Element of COMPLEX n : S1[z1] } = { H2(z2) where z2 is Element of COMPLEX n : S1[z2] }
from FRAENKEL:sch 5(A1);
assume
A <> {}
; dist (x,A) >= 0
then consider z1 being Element of COMPLEX n such that
A3:
z1 in A
by SUBSET_1:4;
A4:
|.(x - z1).| in X
by A3, A2;
dist (x,A) = lower_bound X
by Def17, A2;
hence
dist (x,A) >= 0
by A4, A5, Th112; verum