let X, x, y, z be set ; for O being Order of X st x in X & y in X & z in X & [x,y] in O & [y,z] in O holds
[x,z] in O
let O be Order of X; ( x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O )
field O = X
by Lm4;
then
O is_transitive_in X
by RELAT_2:def 16;
hence
( x in X & y in X & z in X & [x,y] in O & [y,z] in O implies [x,z] in O )
; verum