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 ) by RELAT_2:31; :: 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 )
assume A1: for x, y, z being set st x,y in R & y,z in R holds
x,z in R ; :: thesis: R is transitive
let x, y, z be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )
reconsider xx = x, yy = y, zz = z as set by TARSKI:1;
assume ( x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
then ( xx,yy in R & yy,zz in R ) ;
hence [x,z] in R by A1, MMLQUERY:def 1; :: thesis: verum