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