let X be set ; :: thesis: for T being Tolerance of X holds T c= T * T
let T be Tolerance of X; :: thesis: T c= T * T
let x be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in T or [x,b₁] in T * T )
let y be set ; :: thesis: ( not [x,y] in T or [x,y] in T * T )
assume A1: [x,y] in T ; :: thesis: [x,y] in T * T
then y in X by ZFMISC_1:87;
then [y,y] in T by Th27;
hence [x,y] in T * T by A1, RELAT_1:def 8; :: thesis: verum