let R be Relation; :: thesis: ( R is transitive iff R * R c= R )

hereby :: thesis: ( R * R c= R implies R is transitive )

assume R is transitive ; :: thesis: R * R c= R
then A2: R is_transitive_in field R by Def16;

now :: thesis: for a, b being set st [a,b] in R * R holds
[a,b] in R

let a, b be set ; :: thesis: ( [a,b] in R * R implies [a,b] in R )
assume [a,b] in R * R ; :: thesis: [a,b] in R
then consider c being set such that
A3: [a,c] in R and
A4: [c,b] in R by RELAT_1:def 8;
A5: c in field R by A3, RELAT_1:15;
( a in field R & b in field R ) by A3, A4, RELAT_1:15;
hence [a,b] in R by A2, A3, A4, A5, Def8; :: thesis: verum

end;

hence R * R c= R by RELAT_1:def 3; :: thesis: verum

end;

assume A6: R * R c= R ; :: thesis: R is transitive
let a be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being set st a in field R & y in field R & z in field R & [a,y] in R & [y,z] in R holds
[a,z] in R
let b, c be set ; :: thesis: ( a in field R & b in field R & c in field R & [a,b] in R & [b,c] in R implies [a,c] in R )
assume ( a in field R & b in field R & c in field R ) ; :: thesis: ( not [a,b] in R or not [b,c] in R or [a,c] in R )
assume ( [a,b] in R & [b,c] in R ) ; :: thesis: [a,c] in R
then [a,c] in R * R by RELAT_1:def 8;
hence [a,c] in R by A6; :: thesis: verum