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