let X be set ; :: thesis: for T being Tolerance of X holds T is_reflexive_in X
let T be Tolerance of X; :: thesis: T is_reflexive_in X
field T = X by ORDERS_1:12;
hence T is_reflexive_in X by RELAT_2:def 9; :: thesis: verum