let x, y be Element of M; :: thesis: ( x tolerates y implies y tolerates x )
assume x tolerates y ; :: thesis: y tolerates x
then dist (x,y) = 0 by Def1;
hence y tolerates x by Def1; :: thesis: verum