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