let S, X be non empty set ; :: thesis: for R being Relation of X st R is transitive holds

R is_transitive_in S

let R be Relation of X; :: thesis: ( R is transitive implies R is_transitive_in S )

assume R is transitive ; :: thesis: R is_transitive_in S

then A1: R is_transitive_in field R ;

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in S or not y in S or not z in S or not [x,y] in R or not [y,z] in R or [x,z] in R )

assume ( x in S & y in S & z in S ) ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )

assume A2: [x,y] in R ; :: thesis: ( not [y,z] in R or [x,z] in R )

then A3: x in field R by RELAT_1:15;

assume A4: [y,z] in R ; :: thesis: [x,z] in R

then ( y in field R & z in field R ) by RELAT_1:15;

hence [x,z] in R by A1, A2, A4, A3; :: thesis: verum

R is_transitive_in S

let R be Relation of X; :: thesis: ( R is transitive implies R is_transitive_in S )

assume R is transitive ; :: thesis: R is_transitive_in S

then A1: R is_transitive_in field R ;

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in S or not y in S or not z in S or not [x,y] in R or not [y,z] in R or [x,z] in R )

assume ( x in S & y in S & z in S ) ; :: thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )

assume A2: [x,y] in R ; :: thesis: ( not [y,z] in R or [x,z] in R )

then A3: x in field R by RELAT_1:15;

assume A4: [y,z] in R ; :: thesis: [x,z] in R

then ( y in field R & z in field R ) by RELAT_1:15;

hence [x,z] in R by A1, A2, A4, A3; :: thesis: verum