let x, y, z be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: ( not x in field ((f * R) * (f ")) or not y in field ((f * R) * (f ")) or not z in field ((f * R) * (f ")) or not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") )

assume that

x in field ((f * R) * (f ")) and

y in field ((f * R) * (f ")) and

z in field ((f * R) * (f ")) ; :: thesis: ( not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") )

assume that

A1: [x,y] in (f * R) * (f ") and

A2: [y,z] in (f * R) * (f ") ; :: thesis: [x,z] in (f * R) * (f ")

A3: ( x in dom f & z in dom f ) by A1, A2, Th6;

A4: [(f . y),(f . z)] in R by A2, Th6;

then A5: f . z in field R by RELAT_1:15;

A6: R is_transitive_in field R by RELAT_2:def 16;

A7: [(f . x),(f . y)] in R by A1, Th6;

then ( f . x in field R & f . y in field R ) by RELAT_1:15;

then [(f . x),(f . z)] in R by A7, A4, A5, A6;

hence [x,z] in (f * R) * (f ") by A3, Th6; :: thesis: verum

assume that

x in field ((f * R) * (f ")) and

y in field ((f * R) * (f ")) and

z in field ((f * R) * (f ")) ; :: thesis: ( not [x,y] in (f * R) * (f ") or not [y,z] in (f * R) * (f ") or [x,z] in (f * R) * (f ") )

assume that

A1: [x,y] in (f * R) * (f ") and

A2: [y,z] in (f * R) * (f ") ; :: thesis: [x,z] in (f * R) * (f ")

A3: ( x in dom f & z in dom f ) by A1, A2, Th6;

A4: [(f . y),(f . z)] in R by A2, Th6;

then A5: f . z in field R by RELAT_1:15;

A6: R is_transitive_in field R by RELAT_2:def 16;

A7: [(f . x),(f . y)] in R by A1, Th6;

then ( f . x in field R & f . y in field R ) by RELAT_1:15;

then [(f . x),(f . z)] in R by A7, A4, A5, A6;

hence [x,z] in (f * R) * (f ") by A3, Th6; :: thesis: verum