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 ( x tolerates y & y tolerates z ) ; :: thesis: x tolerates z
then ( dist (x,y) = 0 & dist (y,z) = 0 ) ;
then dist (x,z) <= 0 + 0 by METRIC_1:4;
then dist (x,z) = 0 by METRIC_1:5;
hence x tolerates z ; :: thesis: verum