let X be set ; :: thesis: for x, y, z being object
for R being transitive Tolerance of X st y in Class (R,x) & z in Class (R,x) holds
[y,z] in R
let x, y, z be object ; :: 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, Th19;
then A3: [x,z] in R by Th6;
[y,x] in R by A1, Th19;
hence [y,z] in R by A3, Th7; :: thesis: verum