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

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