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 that
A1: y in Class R,x and
A2: z in Class R,x ; :: thesis: [y,z] in R
[z,x] in R by A2, Th27;
then A3: [x,z] in R by Th12;
[y,x] in R by A1, Th27;
hence [y,z] in R by A3, Th13; :: thesis: verum