ConRelat P,Q is_transitive_in field (ConRelat P,Q)

proof

set X = field (ConRelat P,Q);
set R = ConRelat P,Q;
for x, y, z being set st x in field (ConRelat P,Q) & y in field (ConRelat P,Q) & z in field (ConRelat P,Q) & [x,y] in ConRelat P,Q & [y,z] in ConRelat P,Q holds
[x,z] in ConRelat P,Q

proof

let x, y, z be set ; :: thesis: ( x in field (ConRelat P,Q) & y in field (ConRelat P,Q) & z in field (ConRelat P,Q) & [x,y] in ConRelat P,Q & [y,z] in ConRelat P,Q implies [x,z] in ConRelat P,Q )
assume B0: ( x in field (ConRelat P,Q) & y in field (ConRelat P,Q) & z in field (ConRelat P,Q) & [x,y] in ConRelat P,Q & [y,z] in ConRelat P,Q ) ; :: thesis: [x,z] in ConRelat P,Q
set X1 = ConFuncs P,Q;
B1: field (ConRelat P,Q) c= ConFuncs P,Q by LemConRelat01;
ConRelat P,Q is_transitive_in ConFuncs P,Q by LemConRelat03;
hence [x,z] in ConRelat P,Q by B0, B1, RELAT_2:def 8; :: thesis: verum

end;

hence ConRelat P,Q is_transitive_in field (ConRelat P,Q) by RELAT_2:def 8; :: thesis: verum

end;

hence ConRelat P,Q is transitive by RELAT_2:def 16; :: thesis: verum