let X, y, x, z be set ; :: thesis: for R being transitive Tolerance of X st y in Class R,x & z in Class R,x holds
[y,z] in R
let R be transitive Tolerance of X; :: thesis: ( y in Class R,x & z in Class R,x implies [y,z] in R )
assume ( y in Class R,x & z in Class R,x ) ; :: thesis: [y,z] in R
then ( [y,x] in R & [z,x] in R ) by Th27;
then ( [y,x] in R & [x,z] in R ) by Th12;
hence [y,z] in R by Th13; :: thesis: verum