let R be Relation; :: thesis: ( R is transitive iff for x, y, z being object st [x,y] in R & [y,z] in R holds

[x,z] in R )

thus ( R is transitive implies for x, y, z being object st [x,y] in R & [y,z] in R holds

[x,z] in R ) :: thesis: ( ( for x, y, z being object st [x,y] in R & [y,z] in R holds

[x,z] in R ) implies R is transitive )

[x,z] in R ; :: thesis: R is transitive

then for x, y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds

[x,z] in R ;

then R is_transitive_in field R by RELAT_2:def 8;

hence R is transitive by RELAT_2:def 16; :: thesis: verum

[x,z] in R )

thus ( R is transitive implies for x, y, z being object st [x,y] in R & [y,z] in R holds

[x,z] in R ) :: thesis: ( ( for x, y, z being object st [x,y] in R & [y,z] in R holds

[x,z] in R ) implies R is transitive )

proof

assume
for x, y, z being object st [x,y] in R & [y,z] in R holds
assume
R is transitive
; :: thesis: for x, y, z being object st [x,y] in R & [y,z] in R holds

[x,z] in R

then A1: R is_transitive_in field R by RELAT_2:def 16;

let x, y, z be object ; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )

assume that

A2: [x,y] in R and

A3: [y,z] in R ; :: thesis: [x,z] in R

A4: z in field R by A3, RELAT_1:15;

( x in field R & y in field R ) by A2, RELAT_1:15;

hence [x,z] in R by A1, A2, A3, A4, RELAT_2:def 8; :: thesis: verum

end;[x,z] in R

then A1: R is_transitive_in field R by RELAT_2:def 16;

let x, y, z be object ; :: thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )

assume that

A2: [x,y] in R and

A3: [y,z] in R ; :: thesis: [x,z] in R

A4: z in field R by A3, RELAT_1:15;

( x in field R & y in field R ) by A2, RELAT_1:15;

hence [x,z] in R by A1, A2, A3, A4, RELAT_2:def 8; :: thesis: verum

[x,z] in R ; :: thesis: R is transitive

then for x, y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds

[x,z] in R ;

then R is_transitive_in field R by RELAT_2:def 8;

hence R is transitive by RELAT_2:def 16; :: thesis: verum