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 & [c,b] in R ) by RELAT_1:def 8;
( a in field R & b in field R & c in field R ) by A3, RELAT_1:30;
hence [a,b] in R by A2, A3, Def8; :: thesis: verum

end;

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

end;

now

assume A4: 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 ( a in field R & b in field R & c in field R & [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 A4; :: 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