set P = TolStr(# D,({} (D,D)) #);
thus the ToleranceRel of TolStr(# D,({} (D,D)) #) is_irreflexive_in the carrier of TolStr(# D,({} (D,D)) #) :: according to PCS_0:def 10 :: thesis: TolStr(# D,({} (D,D)) #) is pcs-tol-symmetric

proof

let x be set ; :: according to RELAT_2:def 2 :: thesis: ( not x in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) )
thus ( not x in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) ) ; :: thesis: verum

end;

let x be set ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: for b₁ being set holds
( not x in the carrier of TolStr(# D,({} (D,D)) #) or not b₁ in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) or [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) )
thus for b₁ being set holds
( not x in the carrier of TolStr(# D,({} (D,D)) #) or not b₁ in the carrier of TolStr(# D,({} (D,D)) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) or [^,^] in the ToleranceRel of TolStr(# D,({} (D,D)) #) ) ; :: thesis: verum