let X, x, y, z be set ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: verum