let X be non empty set ; :: thesis: for R being transitive Relation of X
for x, y, z being Element of X st x <=_ R,y & y <=_ R,z holds
x <=_ R,z
let R be transitive Relation of X; :: thesis: for x, y, z being Element of X st x <=_ R,y & y <=_ R,z holds
x <=_ R,z
let x, y, z be Element of X; :: thesis: ( x <=_ R,y & y <=_ R,z implies x <=_ R,z )
assume A: ( x <=_ R,y & y <=_ R,z ) ; :: thesis: x <=_ R,z
then ( x in field R & y in field R & z in field R ) by RELAT_1:15;
hence x <=_ R,z by A, RELAT_2:def 8, RELAT_2:def 16; :: thesis: verum