TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider A9 = A, B9 = B as Subset of (TopSpaceMetr (Euclid n)) ;
take min_dist_min (A9,B9) ; :: thesis: ex A9, B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) )
take A9 ; :: thesis: ex B9 being Subset of (TopSpaceMetr (Euclid n)) st
( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) )
take B9 ; :: thesis: ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) )
thus ( A = A9 & B = B9 & min_dist_min (A9,B9) = min_dist_min (A9,B9) ) ; :: thesis: verum