reconsider A' = A, B' = B as Subset of (TopSpaceMetr (Euclid n)) ;
take min_dist_min A',B' ; :: thesis: ex A', B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & min_dist_min A',B' = min_dist_min A',B' )
take A' ; :: thesis: ex B' being Subset of (TopSpaceMetr (Euclid n)) st
( A = A' & B = B' & min_dist_min A',B' = min_dist_min A',B' )
take B' ; :: thesis: ( A = A' & B = B' & min_dist_min A',B' = min_dist_min A',B' )
thus ( A = A' & B = B' & min_dist_min A',B' = min_dist_min A',B' ) ; :: thesis: verum