let P, Q be non empty strict chain-complete Poset; :: thesis: ConRelat P,Q is_transitive_in ConFuncs P,Q
set X = ConFuncs P,Q;
set R = ConRelat P,Q;
for x, y, z being set 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

proof

let x, y, z be set ; :: thesis: ( 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 implies [x,z] in ConRelat P,Q )
assume B1: ( 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: [x,z] in ConRelat P,Q
consider f, g being Function of P,Q such that
B2: ( x = f & y = g & f <= g ) by B1, DefConRelat;
consider g1, h being Function of P,Q such that
B3: ( y = g1 & z = h & g1 <= h ) by B1, DefConRelat;
f <= h by B3, B2, Lemlessthan02;
hence [x,z] in ConRelat P,Q by B1, B2, B3, DefConRelat; :: thesis: verum

end;

hence ConRelat P,Q is_transitive_in ConFuncs P,Q by RELAT_2:def 8; :: thesis: verum