TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P9 = P, Q9 = Q as Subset of (TopSpaceMetr (Euclid n)) ;
take max_dist_min (P9,Q9) ; :: thesis: ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) )
take P9 ; :: thesis: ex Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) )
take Q9 ; :: thesis: ( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) )
thus ( P = P9 & Q = Q9 & max_dist_min (P9,Q9) = max_dist_min (P9,Q9) ) ; :: thesis: verum