let n be Element of 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) -> 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();
assume A <> {} ; :: thesis: dist (x,A) >= 0
then consider z1 being Element of COMPLEX n such that
A1: z1 in A by SUBSET_1:4;
A2: |.(x - z1).| in X by A1;

A3: now

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 = |.(x - z).| & z in A ) ;
hence r9 >= 0 by Th112; :: thesis: verum

end;

dist (x,A) = lower_bound X by Def20;
hence dist (x,A) >= 0 by A2, A3, Th130; :: thesis: verum