let R be Relation; :: thesis: for X being set st R is_transitive_in X holds
R ~ is_transitive_in X
let X be set ; :: thesis: ( R is_transitive_in X implies R ~ is_transitive_in X )
assume A1: for x, y, z being set st x in X & y in X & z in X & [x,y] in R & [y,z] in R holds
[x,z] in R ; :: according to RELAT_2:def 8 :: thesis: R ~ is_transitive_in X
let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in X or not b₁ in X or not b₂ in X or not [x,b₁] in R ~ or not [b₁,b₂] in R ~ or [x,b₂] in R ~ )
let y, z be set ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in R ~ or not [y,z] in R ~ or [x,z] in R ~ )
assume A2: ( x in X & y in X & z in X & [x,y] in R ~ & [y,z] in R ~ ) ; :: thesis: [x,z] in R ~
then ( [y,x] in R & [z,y] in R ) by RELAT_1:def 7;
then [z,x] in R by A1, A2;
hence [x,z] in R ~ by RELAT_1:def 7; :: thesis: verum