set P = TolStr(# D,(nabla D) #);
set TR = the ToleranceRel of TolStr(# D,(nabla D) #);
A1: field the ToleranceRel of TolStr(# D,(nabla D) #) = the carrier of TolStr(# D,(nabla D) #) by ORDERS_1:97;
hence the ToleranceRel of TolStr(# D,(nabla D) #) is_reflexive_in the carrier of TolStr(# D,(nabla D) #) by RELAT_2:def 9; :: according to PCS_0:def 9 :: thesis: TolStr(# D,(nabla D) #) is pcs-tol-symmetric
thus the ToleranceRel of TolStr(# D,(nabla D) #) is_symmetric_in the carrier of TolStr(# D,(nabla D) #) by A1, RELAT_2:def 11; :: according to PCS_0:def 11 :: thesis: verum