set TR = the ToleranceRel of P;
A1: field the ToleranceRel of P = the carrier of P by ORDERS_1:12;
the ToleranceRel of P is_reflexive_in the carrier of P by Def9;
hence the ToleranceRel of P is reflexive by A1; :: thesis: verum