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