let R be Relation; :: thesis: ( R is transitive iff for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R )
thus ( R is transitive implies for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ) :: thesis: ( ( for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ) implies R is transitive )

proof

assume R is transitive ; :: thesis: for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R
then A1: R is_transitive_in field R by RELAT_2:def 16;
let x, y, z be set ; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume A2: ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( x in field R & y in field R & z in field R ) by RELAT_1:30;
hence [x,z] in R by A1, A2, RELAT_2:def 8; :: thesis: verum

end;

assume for x, y, z being set st [x,y] in R & [y,z] in R holds
[x,z] in R ; :: thesis: R is transitive
then for x, y, z being set st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R ;
then R is_transitive_in field R by RELAT_2:def 8;
hence R is transitive by RELAT_2:def 16; :: thesis: verum