let n be Nat; :: thesis: for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
dist (A,B) >= 0
let A, B be Subset of (COMPLEX n); :: thesis: ( A <> {} & B <> {} implies dist (A,B) >= 0 )
defpred S₁[ set , set ] means ( $1 in A & $2 in B );
deffunc H₁( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;
deffunc H₂( Element of COMPLEX n, Element of COMPLEX n) -> Element of REAL = In (|.($1 - $2).|,REAL);
A1: for z1, z2 being Element of COMPLEX n holds H₁(z1,z2) = H₂(z1,z2) ;
A2: { H₁(z1,z2) where z1, z2 is Element of COMPLEX n : S₁[z1,z2] } = { H₂(z1,z2) where z1, z2 is Element of COMPLEX n : S₁[z1,z2] } from FRAENKEL:sch 7(A1);
reconsider Z = { H₂(z1,z) where z1, z is Element of COMPLEX n : S₁[z1,z] } as Subset of REAL from DOMAIN_1:sch 9();
assume that
A3: A <> {} and
A4: B <> {} ; :: thesis: dist (A,B) >= 0
consider z1 being Element of COMPLEX n such that
A5: z1 in A by A3, SUBSET_1:4;

A6: now :: thesis: for r9 being Real st r9 in Z holds
r9 >= 0

let r9 be Real; :: thesis: ( r9 in Z implies r9 >= 0 )
assume r9 in Z ; :: thesis: r9 >= 0
then ex z1, z being Element of COMPLEX n st
( r9 = |.(z1 - z).| & z1 in A & z in B ) by A2;
hence r9 >= 0 by Th94; :: thesis: verum

end;

consider z2 being Element of COMPLEX n such that
A7: z2 in B by A4, SUBSET_1:4;
A8: dist (A,B) = lower_bound Z by Def19, A2;
|.(z1 - z2).| in Z by A5, A7, A2;
hence dist (A,B) >= 0 by A8, A6, Th112; :: thesis: verum