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

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

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

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

then A1: R is_transitive_in field R ;

end;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

hence
R * R c= R
; :: thesis: verum[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;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

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