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 be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in id X or [x,b₁] in T )
let y be set ; :: 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 Th27; :: thesis: verum