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