let X be non empty set ; :: thesis: for R being Relation of X st R is_transitive_in X holds

R is transitive

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

assume A1: R is_transitive_in X ; :: 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 )

field R c= X \/ X by RELSET_1:8;

hence ( 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 ) by A1; :: thesis: verum

R is transitive

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

assume A1: R is_transitive_in X ; :: 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 )

field R c= X \/ X by RELSET_1:8;

hence ( 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 ) by A1; :: thesis: verum