TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then 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