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