let X, x, y, z be set ; :: thesis: for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R
let R be transitive total Relation of X; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
A1: field R = X by ORDERS_1:97;
assume ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then A2: ( x in X & y in X & z in X & [x,y] in R & [y,z] in R ) by Lm1;
R is_transitive_in X by A1, RELAT_2:def 16;
hence [x,z] in R by A2, RELAT_2:def 8; :: thesis: verum