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 A1: R is_transitive_in field R ;

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

let a, b be object ; :: 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 object such that
A2: [a,c] in R and
A3: [c,b] in R by RELAT_1:def 8;
A4: c in field R by A2, RELAT_1:15;
( a in field R & b in field R ) by A2, A3, RELAT_1:15;
hence [a,b] in R by A1, A2, A3, A4; :: thesis: verum

end;

hence R * R c= R ; :: thesis: verum

end;

assume A5: R * R c= R ; :: thesis: R is transitive
let a be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being object 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 object ; :: 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 A5; :: thesis: verum