let n be Element of NAT ; :: thesis: for A, B being non empty Subset of holds dist_min A,B >= 0
let A, B be non empty Subset of ; :: thesis: dist_min A,B >= 0
ex A', B' being Subset of st
( A = A' & B = B' & dist_min A,B = min_dist_min A',B' ) by Def1;
hence dist_min A,B >= 0 by Th11; :: thesis: verum