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