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
let x be object ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: for b₁ being object 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 object 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