:: deftheorem Def7 defines ConRelat POSET_1:def 7 :
for P, Q being non empty strict chain-complete Poset
for b₃ being Relation of (ConFuncs (P,Q)) holds
( b₃ = ConRelat (P,Q) iff for x, y being set holds
( [x,y] in b₃ iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) );