let n be Nat; :: thesis: 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; :: thesis: for A being Subset of (COMPLEX n) st A <> {} holds
dist (x,A) >= 0
let A be Subset of (COMPLEX n); :: thesis: ( 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 <> {} ; :: thesis: 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;
A5: now :: thesis: for r9 being Real st r9 in X holds
r9 >= 0
let r9 be Real; :: thesis: ( r9 in X implies r9 >= 0 )
assume r9 in X ; :: thesis: r9 >= 0
then ex z being Element of COMPLEX n st
( r9 = H1(z) & z in A ) ;
hence r9 >= 0 by Th94; :: thesis: verum
end;
dist (x,A) = lower_bound X by Def17, A2;
hence dist (x,A) >= 0 by A4, A5, Th112; :: thesis: verum