not the carrier of MS is empty ;
then consider s being object such that
A1: s in the carrier of MS ;
reconsider s = s as Element of MS by A1;
dist (s,s) = 0 by METRIC_1:1;
then [s,s] in fundamental_element_of_entourages (MS,r) ;
hence not fundamental_element_of_entourages (MS,r) is empty ; :: thesis: verum