let M be PseudoMetricSpace; :: thesis: for x, y, z being Element of M st x tolerates y & y tolerates z holds
x tolerates z
let x, y, z be Element of M; :: thesis: ( x tolerates y & y tolerates z implies x tolerates z )
assume A1: ( x tolerates y & y tolerates z ) ; :: thesis: x tolerates z
then A2: dist x,y = 0 by Def1;
dist y,z = 0 by A1, Def1;
then dist x,z <= 0 + 0 by A2, METRIC_1:4;
then dist x,z = 0 by METRIC_1:5;
hence x tolerates z by Def1; :: thesis: verum