let X be set ; :: thesis: for z being object
for R being transitive total Relation of X
for x, y being object st [x,y] in R & [y,z] in R holds
[x,z] in R
let z be object ; :: thesis: for R being transitive total Relation of X
for x, y being object st [x,y] in R & [y,z] in R holds
[x,z] in R
let R be transitive total Relation of X; :: thesis: for x, y being object st [x,y] in R & [y,z] in R holds
[x,z] in R
let x, y be object ; :: 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; :: thesis: verum