let X be set ; :: thesis: for T being Tolerance of X holds id X c= T
let T be Tolerance of X; :: thesis: id X c= T
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in id X or [x,y] in T )
assume [x,y] in id X ; :: thesis: [x,y] in T
then ( x in X & x = y ) by RELAT_1:def 10;
hence [x,y] in T by Th7; :: thesis: verum