let x, y, z be set ; :: 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:30;
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:30;
then [(f . x),(f . z)] in R by A7, A4, A5, A6, RELAT_2:def 8;
hence [x,z] in (f * R) * (f " ) by A3, Th6; :: thesis: verum