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 )
assume that
A1: [x,y] in R and
A2: [y,z] in R ; :: thesis: [x,z] in R
A3: z in X by A2, Lm1;
field R = X by ORDERS_1:12;
then A4: R is_transitive_in X by RELAT_2:def 16;
( x in X & y in X ) by A1, Lm1;
hence [x,z] in R by A1, A2, A3, A4, RELAT_2:def 8; :: thesis: verum