reconsider P' = P, Q' = Q as Subset of (TopSpaceMetr (Euclid n)) ;
take HausDist P',Q' ; :: thesis: ex P', Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & HausDist P',Q' = HausDist P',Q' )
take P' ; :: thesis: ex Q' being Subset of (TopSpaceMetr (Euclid n)) st
( P = P' & Q = Q' & HausDist P',Q' = HausDist P',Q' )
take Q' ; :: thesis: ( P = P' & Q = Q' & HausDist P',Q' = HausDist P',Q' )
thus ( P = P' & Q = Q' & HausDist P',Q' = HausDist P',Q' ) ; :: thesis: verum