A1:
R is_transitive_in field R
by Def16;

let x be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for 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 ~

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

assume that

A2: ( x in field (R ~) & y in field (R ~) ) and

A3: z in field (R ~) and

A4: [x,y] in R ~ and

A5: [y,z] in R ~ ; :: thesis: [x,z] in R ~

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

A7: [y,x] in R by A4, RELAT_1:def 7;

( z in field R & [z,y] in R ) by A3, A5, RELAT_1:21, RELAT_1:def 7;

then [z,x] in R by A1, A6, A7;

hence [x,z] in R ~ by RELAT_1:def 7; :: thesis: verum

let x be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for 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 ~

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

assume that

A2: ( x in field (R ~) & y in field (R ~) ) and

A3: z in field (R ~) and

A4: [x,y] in R ~ and

A5: [y,z] in R ~ ; :: thesis: [x,z] in R ~

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

A7: [y,x] in R by A4, RELAT_1:def 7;

( z in field R & [z,y] in R ) by A3, A5, RELAT_1:21, RELAT_1:def 7;

then [z,x] in R by A1, A6, A7;

hence [x,z] in R ~ by RELAT_1:def 7; :: thesis: verum