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