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 object 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 object ; :: 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 A3: ( 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);
A4: field (ConRelat (P,Q)) c= ConFuncs (P,Q) by Lm13;
ConRelat (P,Q) is_transitive_in ConFuncs (P,Q) by Lm15;
hence [x,z] in ConRelat (P,Q) by A3, A4, 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