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

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