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

A1: now

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

now

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;

now

assume A6: R * R c= R ; :: thesis: R is transitive

now

let a, 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 that
a in field R and
b in field R and
c in field R and
A7: ( [a,b] in R & [b,c] in R ) ; :: thesis: [a,c] in R
[a,c] in R * R by A7, RELAT_1:def 8;
hence [a,c] in R by A6; :: thesis: verum

end;

then R is_transitive_in field R by Def8;
hence R is transitive by Def16; :: thesis: verum

end;

hence ( R is transitive iff R * R c= R ) by A1; :: thesis: verum