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 S₁[ set ] means $1 in A;
deffunc H₁( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H₂( Element of COMPLEX n) -> Real = |.(x - $1).|;
reconsider X = { H₁(z) where z is Element of COMPLEX n : S₁[z] } as Subset of REAL from DOMAIN_1:sch 8();
A1: for z being Element of COMPLEX n holds H₁(z) = H₂(z) ;
A2: { H₁(z1) where z1 is Element of COMPLEX n : S₁[z1] } = { H₂(z2) where z2 is Element of COMPLEX n : S₁[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 = H₁(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