let P, Q be non empty strict chain-complete Poset; :: thesis:
set X = ConFuncs (P,Q);
set R = ConRelat (P,Q);
for x, y, z being object st x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) holds
[x,z] in ConRelat (P,Q)

let x, y, z be object ; :: thesis:
assume A1: ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & z in ConFuncs (P,Q) & [x,y] in ConRelat (P,Q) & [y,z] in ConRelat (P,Q) ) ; :: thesis:
then consider f, g being Function of P,Q such that
A2: ( x = f & y = g & f <= g ) by Def7;
consider g1, h being Function of P,Q such that
A3: ( y = g1 & z = h & g1 <= h ) by A1, Def7;
f <= h by A3, A2, Lm11;
hence [x,z] in ConRelat (P,Q) by A1, A2, A3, Def7; :: thesis:

end;