theorem :: METRIC_2:30

for M being PseudoMetricSpace holds elem_in_rel_1 M = elem_in_rel_2 M