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