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)
; 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
; 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
; ( 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) )
; verum