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

A4: now

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 ) ;
hence r9 >= 0 by Th112; :: thesis: verum

end;

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