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 )
assume A1: ( A <> {} & B <> {} ) ; :: thesis: 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 COMPLSP1:sch 2();
consider z1 being Element of COMPLEX n such that
A2: z1 in A by A1, SUBSET_1:10;
consider z2 being Element of COMPLEX n such that
A3: z2 in B by A1, SUBSET_1:10;
A4: |.(z1 - z2).| in Z by A2, A3;
A5: dist A,B = lower_bound Z by Def20;

now

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

end;

hence dist A,B >= 0 by A4, A5, Th84; :: thesis: verum