let x, y be Element of P; :: thesis: ( (P,x,y) implies (P,y,x) )
assume A1: [x,y] in the ToleranceRel of P ; :: according to PCS_0:def 7 :: thesis: (P,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; :: according to PCS_0:def 7 :: thesis: verum