let x, y be Element of P; :: thesis: ( x (--) y implies y (--) x )
assume A1: [x,y] in the ToleranceRel of P ; :: according to PCS_0:def 7 :: thesis: y (--) x
then A2: x in the carrier of P by ZFMISC_1:87;
the ToleranceRel of P is_symmetric_in the carrier of P by Def11;
hence [y,x] in the ToleranceRel of P by A1, A2, RELAT_2:def 3; :: according to PCS_0:def 7 :: thesis: verum